Commit 2023-06-09 20:52 ee87762b

View on Github →

feat: port Analysis.ODE.PicardLindelof (#4907)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/ODE/PicardLindelof.lean

added theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq

added theorem IsPicardLindelof.norm_le₀

added structure IsPicardLindelof

added theorem PicardLindelof.FunSpace.continuous_vComp

added theorem PicardLindelof.FunSpace.dist_apply_le_dist

added theorem PicardLindelof.FunSpace.dist_iterate_next_apply_le

added theorem PicardLindelof.FunSpace.dist_iterate_next_le

added theorem PicardLindelof.FunSpace.dist_le_of_forall

added theorem PicardLindelof.FunSpace.dist_next_apply_le_of_le

added theorem PicardLindelof.FunSpace.hasDerivWithinAt_next

added theorem PicardLindelof.FunSpace.intervalIntegrable_vComp

added theorem PicardLindelof.FunSpace.map_t₀

added def PicardLindelof.FunSpace.next

added theorem PicardLindelof.FunSpace.next_apply

added theorem PicardLindelof.FunSpace.norm_vComp_le

added theorem PicardLindelof.FunSpace.range_toContinuousMap

added def PicardLindelof.FunSpace.toContinuousMap

added theorem PicardLindelof.FunSpace.uniformInducing_toContinuousMap

added def PicardLindelof.FunSpace.vComp

added theorem PicardLindelof.FunSpace.vComp_apply_coe

added structure PicardLindelof.FunSpace

added theorem PicardLindelof.continuous_proj

added theorem PicardLindelof.dist_t₀_le

added theorem PicardLindelof.exists_contracting_iterate

added theorem PicardLindelof.exists_fixed

added theorem PicardLindelof.exists_solution

added theorem PicardLindelof.norm_le

added def PicardLindelof.proj

added theorem PicardLindelof.proj_coe

added theorem PicardLindelof.proj_of_mem

added def PicardLindelof.tDist

added theorem PicardLindelof.tDist_nonneg

added theorem PicardLindelof.tMin_le_tMax

added structure PicardLindelof

added theorem exists_forall_deriv_at_Ioo_eq_of_contDiffOn_nhds

added theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiff

added theorem exists_isPicardLindelof_const_of_contDiffOn_nhds