UniformInterpolation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.SupportingMapInterpolation.supports_of_finite_affine_maximizers line 16
Source documentation
Finite-affine maximizing selections furnish global supporting maps directly.
```
theorem supports_of_finite_affine_maximizers
    {I F : Type*} [Fintype I] [Nonempty I]
    [NormedAddCommGroup F] [InnerProductSpace ℝ F]
    (y : I → F) (c : I → ℝ) {T : F → F}
    (hactive : ∀ x, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i) :
    Supports (FiniteAffine.potential y c) T := by
…
```
Mentions: OAI.Problem358.FiniteAffine.Maximizes, OAI.Problem358.SupportingMapInterpolation.Supports, OAI.Problem358.FiniteAffine.potential

theorem OAI.Problem358.SupportingMapInterpolation.exists_integral_interpolation_constant line 30

Source documentation

Full quantitative interpolation for bounded supporting maps over an arbitrary compact convex body. Its geometric constant is independent of the potentials, maps, atom counts, masses, and slope separation.

theorem exists_integral_interpolation_constant
    {ι : Type*} [Fintype ι]
    (μ : Measure (EuclideanSpace ℝ ι)) [Measure.IsAddHaarMeasure μ]
    {K : Set (EuclideanSpace ℝ ι)}
    (hKc : IsCompact K) (hK : Convex ℝ K) (hKi : (interior K).Nonempty)
    (L : ℝ) :
    ∃ B : ℝ, 0 ≤ B ∧
      ∀ (u v : EuclideanSpace ℝ ι → ℝ)
        (T S : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι),
      Continuous u → Continuous v → Supports u T → Supports v S →
      Measurable T → Measurable S → (∀ x, ‖T x‖ ≤ L) → (∀ x, ‖S x‖ ≤ L) →
      ∀ h : ℝ, 0 < h →
…

Mentions: OAI.Problem358.SupportingMapInterpolation.Supports

lemma OAI.Problem358.one_third_rpow_cube line 63
Source documentation
The real one-third power is a nonnegative cube root.
```
lemma one_third_rpow_cube {w : ℝ} (hw : 0 ≤ w) :
    (Real.rpow w (1 / 3 : ℝ)) ^ 3 = w := by
…
```
theorem OAI.Problem358.stability_of_slice_bound line 75
Source documentation
The scalar optimization in the gradient-interpolation argument. The hypothesis is the squared slice estimate, valid at every positive scale. This formulation includes zero Wasserstein distance without a limiting argument.
```
theorem stability_of_slice_bound {D w A B : ℝ}
    (hD : 0 ≤ D) (hw : 0 ≤ w) (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hbound : ∀ h : ℝ, 0 < h → D ^ 2 ≤ A * w ^ 2 / h ^ 2 + B * h) :
    D ≤ Real.sqrt (A + B) * Real.rpow w (1 / 3 : ℝ) := by
…
```

theorem OAI.Problem358.stability_of_cubic_bound line 111

Source documentation

A cubic stability estimate implies a one-third Hölder estimate.

theorem stability_of_cubic_bound {D w A : ℝ}
    (hD : 0 ≤ D) (hw : 0 ≤ w) (hA : 0 ≤ A)
    (hbound : D ^ 3 ≤ A * w) :
    D ≤ Real.rpow A (1 / 3 : ℝ) * Real.rpow w (1 / 3 : ℝ) := by
…

theorem OAI.Problem358.stability_of_potential_slice_bound line 122

Source documentation

Combine a Lipschitz bound on potentials with the squared slice estimate.

theorem stability_of_potential_slice_bound {D F w A B P : ℝ}
    (hD : 0 ≤ D) (hF : 0 ≤ F) (hw : 0 ≤ w)
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hP : 0 ≤ P)
    (hpotential : F ≤ P * w)
    (hbound : ∀ h : ℝ, 0 < h → D ^ 2 ≤ A * F ^ 2 / h ^ 2 + B * h) :
    D ≤ Real.sqrt (A * P ^ 2 + B) * Real.rpow w (1 / 3 : ℝ) := by
…

theorem OAI.Problem358.stability_of_local_slice_bound line 141

Source documentation

Small-scale interpolation estimates suffice when a uniform map bound is available. The extra coefficient absorbs all scales larger than H; this is useful when the boundary-strip estimate is obtained by contracting the source inside an interior ball.

theorem stability_of_local_slice_bound {D w A B M H : ℝ}
    (hD : 0 ≤ D) (hw : 0 ≤ w) (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hM : D ≤ M) (hH : 0 < H)
    (hbound : ∀ h : ℝ, 0 < h → h ≤ H →
      D ^ 2 ≤ A * w ^ 2 / h ^ 2 + B * h) :
    D ≤ Real.sqrt (A + (B + M ^ 2 / H)) * Real.rpow w (1 / 3 : ℝ) := by
…

theorem OAI.Problem358.UniformInterpolation.integral_eq line 178
Source documentation
Normalizing the source multiplies every real integral by the same nonnegative scalar. No finiteness assumptions are needed for this identity.
```
theorem integral_eq (f : E d → ℝ) :
    (∫ x, f x ∂uniformMeasure K) =
      ((volume K)⁻¹).toReal * ∫ x in K, f x := by
…
```

theorem OAI.Problem358.UniformInterpolation.mapL2Dist_sq_eq line 184

Source documentation

The squared map distance is the normalized unnormalized-source energy.

theorem mapL2Dist_sq_eq (T S : E d → E d) :
    mapL2Dist (uniformMeasure K) T S ^ 2 =
      ((volume K)⁻¹).toReal * ∫ x in K, ‖T x - S x‖ ^ 2 := by
…

theorem OAI.Problem358.UniformInterpolation.slice_bound_of_raw line 193

Source documentation

Transfer the raw finite-difference estimate to the exact normalized-source and map-distance conventions of the qualified problem.

theorem slice_bound_of_raw
    {T S : E d → E d} {f : E d → ℝ} {A B h : ℝ}
    (hraw : (∫ x in K, ‖T x - S x‖ ^ 2) ≤
      (A / h ^ 2) * (∫ x in K, f x ^ 2) + B * h) :
    mapL2Dist (uniformMeasure K) T S ^ 2 ≤
      (A / h ^ 2) * (∫ x, f x ^ 2 ∂uniformMeasure K) +
        (((volume K)⁻¹).toReal * B) * h := by
…

theorem OAI.Problem358.UniformInterpolation.one_third_bound_of_raw line 209

Source documentation

Raw volume interpolation plus a normalized squared-potential estimate implies the desired one-third bound, including zero target distance.

theorem one_third_bound_of_raw
    {T S : E d → E d} {f : E d → ℝ} {A B P w : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hw : 0 ≤ w)
    (hpotential : (∫ x, f x ^ 2 ∂uniformMeasure K) ≤ P ^ 2 * w ^ 2)
    (hraw : ∀ h : ℝ, 0 < h → (∫ x in K, ‖T x - S x‖ ^ 2) ≤
      (A / h ^ 2) * (∫ x in K, f x ^ 2) + B * h) :
    mapL2Dist (uniformMeasure K) T S ≤
      Real.sqrt (A * P ^ 2 + ((volume K)⁻¹).toReal * B) *
        Real.rpow w (1 / 3 : ℝ) := by
…

theorem OAI.Problem358.UniformInterpolation.one_third_bound_of_raw_of_potential line 231

Source documentation

Norm-form version matching the manuscript's Lipschitz potential estimate.

theorem one_third_bound_of_raw_of_potential
    {T S : E d → E d} {f : E d → ℝ} {A B P w : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hP : 0 ≤ P) (hw : 0 ≤ w)
    (hpotential : Real.sqrt (∫ x, f x ^ 2 ∂uniformMeasure K) ≤ P * w)
    (hraw : ∀ h : ℝ, 0 < h → (∫ x in K, ‖T x - S x‖ ^ 2) ≤
      (A / h ^ 2) * (∫ x in K, f x ^ 2) + B * h) :
    mapL2Dist (uniformMeasure K) T S ≤
      Real.sqrt (A * P ^ 2 + ((volume K)⁻¹).toReal * B) *
        Real.rpow w (1 / 3 : ℝ) := by
…

theorem OAI.Problem358.UniformInterpolation.supports_add_const line 261
Source documentation
Adding a constant to a potential does not change its supporting map.
```
theorem supports_add_const {d : ℕ} {u : E d → ℝ} {T : E d → E d}
    (hu : Supports u T) (c : ℝ) : Supports (fun x => u x + c) T := by
…
```

theorem OAI.Problem358.UniformInterpolation.exists_normalized_one_third_constant line 271

Source documentation

The full normalized interpolation theorem, with no residual geometric or finite-difference hypotheses. The potential estimate may be supplied modulo an arbitrary additive constant, as in a variance bound.

theorem exists_normalized_one_third_constant
    {d : ℕ} {K : Set (E d)}
    (hKc : IsCompact K) (hK : Convex ℝ K) (hKi : (interior K).Nonempty)
    (L P : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧
      ∀ (u v : E d → ℝ) (T S : E d → E d),
      Continuous u → Continuous v → Supports u T → Supports v S →
      Measurable T → Measurable S → (∀ x, ‖T x‖ ≤ L) → (∀ x, ‖S x‖ ≤ L) →
      ∀ w : ℝ, 0 ≤ w →
      (∃ c : ℝ, (∫ x, (u x - v x - c) ^ 2 ∂uniformMeasure K) ≤ P ^ 2 * w ^ 2) →
      mapL2Dist (uniformMeasure K) T S ≤ C * Real.rpow w (1 / 3 : ℝ) := by
…