OAI/Analysis/Brenier/SliceInterpolation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.slice_interpolation_of_errors line 14

   Source documentation

   The one-dimensional interpolation estimate, expressed through the two nonnegative secant errors. This is the analytic assembly step before applying convexity to produce the errors.

   theorem slice_interpolation_of_errors
       {f g δ₀ δ₁ : ℝ → ℝ} {a b h L : ℝ}
       (hh : 0 < h) (habh : h ≤ b - a) (_hL : 0 ≤ L)
       (hf : IntervalIntegrable (fun t => (f t) ^ 2) volume a b)
       (hfmeas : AEStronglyMeasurable f volume)
       (hg : IntervalIntegrable (fun t => (g t) ^ 2) volume a b)
       (hδ₀ : IntervalIntegrable (fun t => (δ₀ t) ^ 2) volume a (b - h))
       (hδ₁ : IntervalIntegrable (fun t => (δ₁ t) ^ 2) volume a (b - h))
       (herror₀ : (∫ t in a..b - h, (δ₀ t) ^ 2) ≤ 4 * L ^ 2 * h)
       (herror₁ : (∫ t in a..b - h, (δ₁ t) ^ 2) ≤ 4 * L ^ 2 * h)
       (hdecomp : ∀ t ∈ Icc a (b - h),
         g t = (f (t + h) - f t) / h - δ₀ t + δ₁ t)
   …

2. theorem OAI.Problem358.slice_interpolation_short line 80

   Source documentation

   On a slice shorter than the finite-difference increment, the uniform bound alone suffices.

   theorem slice_interpolation_short
       {f g : ℝ → ℝ} {a b h L : ℝ}
       (hab : a ≤ b) (hh : 0 < h) (hshort : b - a ≤ h)
       (_hf : IntervalIntegrable (fun t => (f t) ^ 2) volume a b)
       (hg : IntervalIntegrable (fun t => (g t) ^ 2) volume a b)
       (hbound : ∀ t ∈ Icc a b, |g t| ≤ 2 * L) :
       (∫ t in a..b, (g t) ^ 2) ≤
         12 / h ^ 2 * (∫ t in a..b, (f t) ^ 2) + 28 * L ^ 2 * h := by
   …

3. theorem OAI.Problem358.intervalIntegrable_sq_of_abs_le line 102

   Source documentation

   A measurable function bounded on a compact interval has integrable square.

   theorem intervalIntegrable_sq_of_abs_le
       {g : ℝ → ℝ} {a b M : ℝ} (hab : a ≤ b) (_hM : 0 ≤ M)
       (hg : Measurable g) (hbound : ∀ t ∈ Icc a b, |g t| ≤ M) :
       IntervalIntegrable (fun t => (g t) ^ 2) volume a b := by
   …

4. theorem OAI.Problem358.slice_interpolation_of_secant_bounds_ae line 119

   Source documentation

   One-dimensional convex-gradient interpolation from the precise secant inequalities. The statement allows every positive increment, including those longer than the interval.

   theorem slice_interpolation_of_secant_bounds_ae
       {u₀ u₁ g₀ g₁ : ℝ → ℝ} {a b h L : ℝ}
       (hab : a ≤ b) (hh : 0 < h) (hL : 0 ≤ L)
       (hu₀ : Measurable u₀) (hu₁ : Measurable u₁)
       (hg₀meas : Measurable g₀) (hg₁meas : Measurable g₁)
       (hf : IntervalIntegrable (fun t => (u₀ t - u₁ t) ^ 2) volume a b)
       (hg₀ : IntervalIntegrable g₀ volume a b)
       (hg₁ : IntervalIntegrable g₁ volume a b)
       (hbound₀ : ∀ t ∈ Icc a b, |g₀ t| ≤ L)
       (hbound₁ : ∀ t ∈ Icc a b, |g₁ t| ≤ L)
       (hsecant₀ : ∀ᵐ t ∂volume.restrict (Icc a (b - h)),
         0 ≤ (u₀ (t + h) - u₀ t) / h - g₀ t ∧
   …

5. theorem OAI.Problem358.slice_interpolation_of_secant_bounds line 176

   Source documentation

   Pointwise secant bounds are a special case of the almost-everywhere estimate.

   theorem slice_interpolation_of_secant_bounds
       {u₀ u₁ g₀ g₁ : ℝ → ℝ} {a b h L : ℝ}
       (hab : a ≤ b) (hh : 0 < h) (hL : 0 ≤ L)
       (hu₀ : Measurable u₀) (hu₁ : Measurable u₁)
       (hg₀meas : Measurable g₀) (hg₁meas : Measurable g₁)
       (hf : IntervalIntegrable (fun t => (u₀ t - u₁ t) ^ 2) volume a b)
       (hg₀ : IntervalIntegrable g₀ volume a b)
       (hg₁ : IntervalIntegrable g₁ volume a b)
       (hbound₀ : ∀ t ∈ Icc a b, |g₀ t| ≤ L)
       (hbound₁ : ∀ t ∈ Icc a b, |g₁ t| ≤ L)
       (hsecant₀ : ∀ t ∈ Icc a (b - h),
         0 ≤ (u₀ (t + h) - u₀ t) / h - g₀ t ∧
   …

6. theorem OAI.Problem358.ae_convex_secant_bounds line 212

   Source documentation

   The unsquared convex secant sandwich holds off a null set, simultaneously at the two endpoints of a fixed positive increment.

   theorem ae_convex_secant_bounds {u : ℝ → ℝ} {L : ℝ≥0}
       (hu : ConvexOn ℝ univ u) (hLip : LipschitzWith L u)
       {h : ℝ} (hh : 0 < h) :
       ∀ᵐ x : ℝ, 0 ≤ (u (x + h) - u x) / h - deriv u x ∧
         (u (x + h) - u x) / h - deriv u x ≤ deriv u (x + h) - deriv u x := by
   …

7. theorem OAI.Problem358.convex_lipschitz_slice_interpolation line 229

   Source documentation

   Concrete one-dimensional gradient interpolation for globally convex Lipschitz potentials. No secant, differentiability, or integrability assumptions are left as hypotheses.

   theorem convex_lipschitz_slice_interpolation {u v : ℝ → ℝ} {L : ℝ≥0}
       (hu : ConvexOn ℝ univ u) (hv : ConvexOn ℝ univ v)
       (hLipU : LipschitzWith L u) (hLipV : LipschitzWith L v)
       {a b h : ℝ} (hab : a ≤ b) (hh : 0 < h) :
       (∫ t in a..b, (deriv u t - deriv v t) ^ 2) ≤
         12 / h ^ 2 * (∫ t in a..b, (u t - v t) ^ 2) + 28 * (L : ℝ) ^ 2 * h := by
   …