OAI/Analysis/Brenier/SupportingInterpolation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.SupportingMapInterpolation.Supports line 15

   Source documentation

   A globally supporting selection; finite affine maximizers satisfy this directly.

   def Supports (u : F → ℝ) (T : F → F) : Prop :=
   …

2. def OAI.Problem358.SupportingMapInterpolation.quotient line 18
3. def OAI.Problem358.SupportingMapInterpolation.slope line 21
4. lemma OAI.Problem358.SupportingMapInterpolation.slope_le_quotient_le_shift line 25

   Source documentation

   Supporting inequalities at the two ends sandwich the forward quotient. This avoids all differentiability and null-set choices in finite-map interpolation.

   lemma slope_le_quotient_le_shift {u : F → ℝ} {T : F → F}
       (hs : Supports u T) {h : ℝ} (hh : 0 < h) (e x : F) :
       slope T e x ≤ quotient u h e x ∧
         quotient u h e x ≤ slope T e (x + h • e) := by
   …

   Mentions: OAI.Problem358.SupportingMapInterpolation.Supports, OAI.Problem358.SupportingMapInterpolation.slope, OAI.Problem358.SupportingMapInterpolation.quotient

5. lemma OAI.Problem358.SupportingMapInterpolation.slope_monotone_shift line 44
6. lemma OAI.Problem358.SupportingMapInterpolation.abs_slope_le line 50
7. lemma OAI.Problem358.SupportingMapInterpolation.quotient_error_sq_le line 59

   Source documentation

   Squared quotient error is controlled by the monotone slope increment.

   lemma quotient_error_sq_le {u : F → ℝ} {T : F → F}
       (hs : Supports u T) {h L : ℝ} (hh : 0 < h)
       (hL : ∀ x, ‖T x‖ ≤ L) {e : F} (he : ‖e‖ ≤ 1) (x : F) :
       (quotient u h e x - slope T e x) ^ 2 ≤
         2 * L * (slope T e (x + h • e) - slope T e x) := by
   …

   Mentions: OAI.Problem358.SupportingMapInterpolation.Supports, OAI.Problem358.SupportingMapInterpolation.quotient, OAI.Problem358.SupportingMapInterpolation.slope

8. lemma OAI.Problem358.SupportingMapInterpolation.quotient_sub line 73
9. lemma OAI.Problem358.SupportingMapInterpolation.slope_difference_sq_le line 79

   Source documentation

   The pointwise estimate whose integral gives cubic-root map stability.

   lemma slope_difference_sq_le {u v : F → ℝ} {T S : F → F}
       (hu : Supports u T) (hv : Supports v S) {h L : ℝ} (hh : 0 < h)
       (hT : ∀ x, ‖T x‖ ≤ L) (hS : ∀ x, ‖S x‖ ≤ L)
       {e : F} (he : ‖e‖ ≤ 1) (x : F) :
       (slope T e x - slope S e x) ^ 2 ≤
         3 * (quotient (fun z => u z - v z) h e x) ^ 2 +
         6 * L * ((slope T e (x + h • e) - slope T e x) +
           (slope S e (x + h • e) - slope S e x)) := by
   …

   Mentions: OAI.Problem358.SupportingMapInterpolation.Supports, OAI.Problem358.SupportingMapInterpolation.slope, OAI.Problem358.SupportingMapInterpolation.quotient

10. lemma OAI.Problem358.SupportingMapInterpolation.slope_difference_sq_le_four line 97
11. lemma OAI.Problem358.SupportingMapInterpolation.measurable_slope line 115
12. lemma OAI.Problem358.SupportingMapInterpolation.integrableOn_slope line 121
13. lemma OAI.Problem358.SupportingMapInterpolation.integrableOn_slope_difference_sq line 129
14. theorem OAI.Problem358.SupportingMapInterpolation.integral_slope_difference_sq_le line 144

    Source documentation

    A derivative-free directional interpolation estimate. All geometry of the source is isolated in the lost mass of its translation core.

    theorem integral_slope_difference_sq_le
        {u v : F → ℝ} {T S : F → F}
        (hu : Supports u T) (hv : Supports v S)
        (hT : Measurable T) (hS : Measurable S)
        {K : Set F} (hK : MeasurableSet K) (hKfin : μ K ≠ ⊤)
        {L h : ℝ} (hTL : ∀ x, ‖T x‖ ≤ L) (hSL : ∀ x, ‖S x‖ ≤ L)
        (hh : 0 < h) {e : F} (he : ‖e‖ ≤ 1)
        (hfm : Measurable (fun x => u x - v x))
        (hf : IntegrableOn (fun x => (u x - v x) ^ 2) K μ) :
        (∫ x in K, (slope T e x - slope S e x) ^ 2 ∂μ) ≤
          (12 / h ^ 2) * (∫ x in K, (u x - v x) ^ 2 ∂μ) +
          28 * L ^ 2 * μ.real (K \ (K ∩ (fun x => x + h • e) ⁻¹' K)) := by
    …

    Mentions: OAI.Problem358.SupportingMapInterpolation.Supports, OAI.Problem358.SupportingMapInterpolation.slope

15. theorem OAI.Problem358.SupportingMapInterpolation.integral_norm_sub_sq_le_of_boundary_strip line 241

    Source documentation

    Summing the directional estimate gives full-dimensional interpolation for bounded supporting maps. Only a linear boundary-strip estimate is needed.

    theorem integral_norm_sub_sq_le_of_boundary_strip
        {u v : EuclideanSpace ℝ ι → ℝ}
        {T S : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
        (hu : Supports u T) (hv : Supports v S)
        (hT : Measurable T) (hS : Measurable S)
        {K : Set (EuclideanSpace ℝ ι)} (hK : MeasurableSet K) (hKfin : μ K ≠ ⊤)
        {L C h : ℝ} (hTL : ∀ x, ‖T x‖ ≤ L) (hSL : ∀ x, ‖S x‖ ≤ L)
        (hh : 0 < h)
        (hfm : Measurable (fun x => u x - v x))
        (hf : IntegrableOn (fun x => (u x - v x) ^ 2) K μ)
        (hstrip : ∀ e : EuclideanSpace ℝ ι, ‖e‖ ≤ 1 →
          μ.real {x | x ∈ K ∧ x + h • e ∉ K} ≤ C * h) :
    …

    Mentions: OAI.Problem358.SupportingMapInterpolation.Supports