Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 21:07 773a7a42

View on Github →

feat(analysis/ODE): prove Picard-Lindelöf/Cauchy-Lipschitz Theorem (#9791)

Estimated changes

Modified docs/undergrad.yaml

Created src/analysis/ODE/picard_lindelof.lean

added theorem exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous

added theorem picard_lindelof.continuous_proj

added theorem picard_lindelof.dist_t₀_le

added theorem picard_lindelof.exists_contracting_iterate

added theorem picard_lindelof.exists_fixed

added theorem picard_lindelof.exists_solution

added theorem picard_lindelof.fun_space.continuous_v_comp

added theorem picard_lindelof.fun_space.dist_apply_le_dist

added theorem picard_lindelof.fun_space.dist_iterate_next_apply_le

added theorem picard_lindelof.fun_space.dist_iterate_next_le

added theorem picard_lindelof.fun_space.dist_le_of_forall

added theorem picard_lindelof.fun_space.dist_next_apply_le_of_le

added theorem picard_lindelof.fun_space.has_deriv_within_at_next

added theorem picard_lindelof.fun_space.interval_integrable_v_comp

added theorem picard_lindelof.fun_space.map_t₀

added def picard_lindelof.fun_space.next

added theorem picard_lindelof.fun_space.next_apply

added theorem picard_lindelof.fun_space.norm_v_comp_le

added theorem picard_lindelof.fun_space.range_to_continuous_map

added def picard_lindelof.fun_space.to_continuous_map

added theorem picard_lindelof.fun_space.uniform_inducing_to_continuous_map

added def picard_lindelof.fun_space.v_comp

added theorem picard_lindelof.fun_space.v_comp_apply_coe

added structure picard_lindelof.fun_space

added theorem picard_lindelof.norm_le

added def picard_lindelof.proj

added theorem picard_lindelof.proj_coe

added theorem picard_lindelof.proj_of_mem

added def picard_lindelof.t_dist

added theorem picard_lindelof.t_dist_nonneg

added theorem picard_lindelof.t_min_le_t_max

added structure picard_lindelof

Modified src/data/set/intervals/unordered_interval.lean

added theorem set.interval_subset_Icc

Modified src/topology/order.lean