Local coefficient bounds with an explicit smallness margin for the BVP estimate.

theorem PlanarMidpoint.local_coefficient_bounds {Ω : Set E} {C : E → Coeff} {p : E} (hΩ : IsOpen Ω) (hp : p ∈ Ω) (hC : ContDiffOn ℝ 2 C Ω) : ∃ r > 0, ∃ M ≥ 0, ∃ L ≥ 0, Metric.ball p r ⊆ Ω ∧ (∀ x ∈ Metric.ball p r, ‖C x‖ ≤ M) ∧ (∀ x ∈ Metric.ball p r, ∀ y ∈ Metric.ball p r, ‖C x - C y‖ ≤ L * ‖x - y‖) ∧ 8 * L * r ^ 2 + 16 * M * r < 1 / 2