Revision #2162 → #2625 · back to history
modifiedPicard operator is a contraction (after restricting the interval)220b90e3a80a
| Field | From #2162 | To #2625 |
|---|
| mathlib.decl | IsPicardLindelof.FunSpace.exists_contractingWith_iterate_next | ODE.FunSpace.exists_contractingWith_iterate_next |
| provenance | ai | ai-moderated |
modifiedIterate bound for the Picard operator (Γᵐ)7ddd5897d338
| Field | From #2162 | To #2625 |
|---|
| mathlib.decl | IsPicardLindelof.FunSpace.dist_iterate_next_apply_le | ODE.FunSpace.dist_iterate_next_apply_le |
| provenance | ai | ai-moderated |