ClosedPaths.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.finite_affine_path_L2_bound_of_closedCell line 15

Source documentation

The finite-affine time estimate stated directly in terms of genuine closed cell masses. A jointly measurable maximizing selector and its exact masses are constructed internally. Injectivity is required only on the interval of use.

theorem finite_affine_path_L2_bound_of_closedCell
    {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
    [MeasurableSpace ι] [MeasurableSingletonClass ι]
    {K : Set (E d)} (hK : MeasurableSet K)
    [IsFiniteMeasure (uniformMeasure K)]
    (y v : ι → ℝ → E d) (c r : ι → ℝ → ℝ) (m : ι → ℝ)
    {a b w κ : ℝ} {R A B : ℝ≥0}
    (hab : a < b) (hw : 0 ≤ w) (hκ : 0 ≤ κ)
    (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hy : ∀ i, Measurable (y i)) (hc : ∀ i, Measurable (c i))
    (hv : ∀ i, Measurable (v i)) (hr : ∀ i, Measurable (r i))
    (hdy : ∀ i q, q ∈ Icc a b → HasDerivAt (y i) (v i q) q)
…

theorem OAI.Problem358.one_third_stability_of_closedCell_intercept_paths line 70

Source documentation

Complete stability from the genuine geometric intercept-path assertion. All endpoint construction, finite optimal coupling, potential interpolation, optimal-map uniqueness and finite-to-general approximation are discharged. The remaining premise is precisely a normalized positive closed-cell path with its weighted derivative-energy bound.

theorem one_third_stability_of_closedCell_intercept_paths
    {d : ℕ} {K Y : Set (E d)}
    (hK : IsCompact K) (hKconv : Convex ℝ K)
    (hKint : (interior K).Nonempty) (hY : IsCompact Y) (hYne : Y.Nonempty)
    (R L : ℝ≥0) (hxR : ∀ᵐ x ∂uniformMeasure K, ‖x‖ ≤ R)
    (hYL : ∀ z ∈ Y, ‖z‖ ≤ L) {κ : ℝ} (hκ : 0 ≤ κ)
    (hpaths : ∀ (n : ℕ), 0 < n →
      ∀ (m : Fin n → ℝ) (y z : Fin n → E d),
      (∀ i, 0 < m i) → (∑ i, m i) = 1 →
      (∀ i, ‖y i‖ ≤ L) → (∀ i, ‖z i‖ ≤ L) →
      (∀ t : ℝ, 0 < t → t < 1 →
        Function.Injective (fun i => (1-t) • y i + t • z i)) →
…