Commit 2023-06-05 05:13 dd381f63

View on Github →

feat: port Analysis.ODE.Gronwall (#4672)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/ODE/Gronwall.lean

added theorem ODE_solution_unique

added theorem ODE_solution_unique_of_mem_set

added theorem dist_le_of_approx_trajectories_ODE

added theorem dist_le_of_approx_trajectories_ODE_of_mem_set

added theorem dist_le_of_trajectories_ODE

added theorem dist_le_of_trajectories_ODE_of_mem_set

added theorem gronwallBound_K0

added theorem gronwallBound_continuous_ε

added theorem gronwallBound_of_K_ne_0

added theorem gronwallBound_x0

added theorem gronwallBound_ε0

added theorem gronwallBound_ε0_δ0

added theorem hasDerivAt_gronwallBound

added theorem hasDerivAt_gronwallBound_shift

added theorem le_gronwallBound_of_liminf_deriv_right_le

added theorem norm_le_gronwallBound_of_norm_deriv_right_le