Difference.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Pointwise estimates for convex forward difference quotients

These are the pointwise ingredients of the coordinate-slice gradient interpolation argument. They do not assert an almost-everywhere derivative existence result or any of the transport theorems.

theorem OAI.Problem358.forwardDifference_sq_control line 13

Source documentation

Translation of a finite difference controls its squared interval integral by the squared integral of the original function.

theorem forwardDifference_sq_control
    {f : ℝ → ℝ} {a b h : ℝ} (hh : 0 < h) (habh : h ≤ b - a)
    (hf : IntervalIntegrable (fun t => (f t) ^ 2) volume a b)
    (hfmeas : AEStronglyMeasurable f volume) :
    IntervalIntegrable (fun t => ((f (t + h) - f t) / h) ^ 2) volume a (b - h) ∧
    (∫ t in a..b - h, ((f (t + h) - f t) / h) ^ 2) ≤
      4 / h ^ 2 * ∫ t in a..b, (f t) ^ 2 := by
…

theorem OAI.Problem358.intervalIntegrable_forwardDifference_sq line 76

Source documentation

Square-integrability of a forward difference quotient on the shortened interval.

theorem intervalIntegrable_forwardDifference_sq
    {f : ℝ → ℝ} {a b h : ℝ} (hh : 0 < h) (habh : h ≤ b - a)
    (hf : IntervalIntegrable (fun t => (f t) ^ 2) volume a b)
    (hfmeas : AEStronglyMeasurable f volume) :
    IntervalIntegrable (fun t => ((f (t + h) - f t) / h) ^ 2) volume a (b - h) :=
…

theorem OAI.Problem358.integral_forwardDifference_sq_le line 85

Source documentation

The squared norm of a forward difference is bounded by four times the squared norm of the function, divided by the squared increment.

theorem integral_forwardDifference_sq_le
    {f : ℝ → ℝ} {a b h : ℝ} (hh : 0 < h) (habh : h ≤ b - a)
    (hf : IntervalIntegrable (fun t => (f t) ^ 2) volume a b)
    (hfmeas : AEStronglyMeasurable f volume) :
    (∫ t in a..b - h, ((f (t + h) - f t) / h) ^ 2) ≤
      4 / h ^ 2 * ∫ t in a..b, (f t) ^ 2 :=
…

def OAI.Problem358.forwardQuotient line 110
Source documentation
Forward difference quotient with step h.
```
def forwardQuotient (u : ℝ → ℝ) (h x : ℝ) : ℝ :=
…
```

theorem OAI.Problem358.convex_forwardQuotient_bounds line 115

Source documentation

Convexity sandwiches a positive-step quotient between the two endpoint derivatives.

theorem convex_forwardQuotient_bounds {S : Set ℝ} {u : ℝ → ℝ}
    {x h p q : ℝ} (hu : ConvexOn ℝ S u)
    (hx : x ∈ S) (hxh : x + h ∈ S) (hh : 0 < h)
    (hp : HasDerivAt u p x) (hq : HasDerivAt u q (x + h)) :
    p ≤ forwardQuotient u h x ∧ forwardQuotient u h x ≤ q := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.convex_forwardQuotient_error_bounds line 129

Source documentation

The nonnegative quotient error is dominated by the derivative increment, which is at most twice the derivative bound.

theorem convex_forwardQuotient_error_bounds {S : Set ℝ} {u : ℝ → ℝ}
    {x h p q L : ℝ} (hu : ConvexOn ℝ S u)
    (hx : x ∈ S) (hxh : x + h ∈ S) (hh : 0 < h)
    (hp : HasDerivAt u p x) (hq : HasDerivAt u q (x + h))
    (hpL : |p| ≤ L) (hqL : |q| ≤ L) :
    0 ≤ forwardQuotient u h x - p ∧
      forwardQuotient u h x - p ≤ q - p ∧ q - p ≤ 2 * L := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.convex_forwardQuotient_error_sq_le line 143

Source documentation

Squared quotient error is controlled by the derivative increment. This is the integrand estimate used before translation cancellation on a slice.

theorem convex_forwardQuotient_error_sq_le {S : Set ℝ} {u : ℝ → ℝ}
    {x h p q L : ℝ} (hu : ConvexOn ℝ S u)
    (hx : x ∈ S) (hxh : x + h ∈ S) (hh : 0 < h)
    (hp : HasDerivAt u p x) (hq : HasDerivAt u q (x + h))
    (hpL : |p| ≤ L) (hqL : |q| ≤ L) :
    (forwardQuotient u h x - p) ^ 2 ≤ 2 * L * (q - p) := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.forwardQuotient_sub line 160

Source documentation

Forward quotients commute with subtraction.

theorem forwardQuotient_sub (u v : ℝ → ℝ) (h x : ℝ) :
    forwardQuotient (fun t => u t - v t) h x =
      forwardQuotient u h x - forwardQuotient v h x := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.derivative_difference_sq_le_quotient_errors line 168

Source documentation

Pointwise decomposition bound for the difference of two derivatives. The two last terms are the respective forward quotient errors.

theorem derivative_difference_sq_le_quotient_errors
    (u v : ℝ → ℝ) (h x p q : ℝ) :
    (p - q) ^ 2 ≤ 3 *
      ((forwardQuotient (fun t => u t - v t) h x) ^ 2 +
        (forwardQuotient u h x - p) ^ 2 +
        (forwardQuotient v h x - q) ^ 2) := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.forwardQuotient_sq_le line 182
Source documentation
A difference quotient is bounded by the two endpoint function values.
```
theorem forwardQuotient_sq_le (u : ℝ → ℝ) (h x : ℝ) :
    (forwardQuotient u h x) ^ 2 ≤
      2 / h ^ 2 * ((u (x + h)) ^ 2 + (u x) ^ 2) := by
…
```
Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.convex_derivative_difference_sq_le line 198

Source documentation

Combined pointwise estimate for two convex functions. Integrating the last two derivative increments is the cancellation step of the slice proof.

theorem convex_derivative_difference_sq_le {S : Set ℝ} {u v : ℝ → ℝ}
    {x h p₀ p₁ q₀ q₁ L : ℝ}
    (hu : ConvexOn ℝ S u) (hv : ConvexOn ℝ S v)
    (hx : x ∈ S) (hxh : x + h ∈ S) (hh : 0 < h)
    (hp₀ : HasDerivAt u p₀ x) (hq₀ : HasDerivAt u q₀ (x + h))
    (hp₁ : HasDerivAt v p₁ x) (hq₁ : HasDerivAt v q₁ (x + h))
    (hp₀L : |p₀| ≤ L) (hq₀L : |q₀| ≤ L)
    (hp₁L : |p₁| ≤ L) (hq₁L : |q₁| ≤ L) :
    (p₀ - p₁) ^ 2 ≤
      6 / h ^ 2 * ((u (x + h) - v (x + h)) ^ 2 + (u x - v x) ^ 2) +
        6 * L * ((q₀ - p₀) + (q₁ - p₁)) := by
…

theorem OAI.Problem358.integrable_translation_sub_sq line 235

Source documentation

A measurable square-integrable function has a square-integrable translate difference.

theorem integrable_translation_sub_sq (f : G → ℝ) (v : G) (hfm : Measurable f)
    (hf : Integrable (fun x => (f x) ^ 2) μ) :
    Integrable (fun x => (f (x + v) - f x) ^ 2) μ := by
…

theorem OAI.Problem358.integrableOn_translation_sub_sq line 249

Source documentation

Local square-integrability on the common translation domain.

theorem integrableOn_translation_sub_sq (K : Set G) (hK : MeasurableSet K)
    (f : G → ℝ) (v : G) (hfm : Measurable f)
    (hf : IntegrableOn (fun x => (f x) ^ 2) K μ) :
    IntegrableOn (fun x => (f (x + v) - f x) ^ 2)
      (K ∩ (fun x => x + v) ⁻¹' K) μ := by
…

theorem OAI.Problem358.integrableOn_translation_quotient_sq line 268

Source documentation

Local square-integrability of the divided finite difference.

theorem integrableOn_translation_quotient_sq (K : Set G) (hK : MeasurableSet K)
    (f : G → ℝ) (v : G) (h : ℝ) (hfm : Measurable f)
    (hf : IntegrableOn (fun x => (f x) ^ 2) K μ) :
    IntegrableOn (fun x => ((f (x + v) - f x) / h) ^ 2)
      (K ∩ (fun x => x + v) ⁻¹' K) μ := by
…

theorem OAI.Problem358.integral_translation_sub_sq_le line 277
Source documentation
Translation does not increase the squared L² finite difference by more than four times the original squared norm. No differentiability is required.
```
theorem integral_translation_sub_sq_le (f : G → ℝ) (v : G)
    (hf : Integrable (fun x => (f x) ^ 2) μ) :
    (∫ x, (f (x + v) - f x) ^ 2 ∂μ) ≤ 4 * ∫ x, (f x) ^ 2 ∂μ := by
…
```

theorem OAI.Problem358.setIntegral_translation_sub_sq_le line 298

Source documentation

The finite-difference contribution on the set where both endpoints belong to K is controlled by the potential's squared norm on K.

theorem setIntegral_translation_sub_sq_le (K : Set G) (hK : MeasurableSet K)
    (f : G → ℝ) (v : G) (hf : IntegrableOn (fun x => (f x) ^ 2) K μ) :
    (∫ x in K ∩ (fun x => x + v) ⁻¹' K, (f (x + v) - f x) ^ 2 ∂μ) ≤
      4 * ∫ x in K, (f x) ^ 2 ∂μ := by
…

theorem OAI.Problem358.setIntegral_translation_quotient_sq_le line 336

Source documentation

The divided finite-difference estimate used in the gradient interpolation argument. It is valid for every real scale (including the harmless zero case).

theorem setIntegral_translation_quotient_sq_le (K : Set G) (hK : MeasurableSet K)
    (f : G → ℝ) (v : G) (h : ℝ)
    (hf : IntegrableOn (fun x => (f x) ^ 2) K μ) :
    (∫ x in K ∩ (fun x => x + v) ⁻¹' K, ((f (x + v) - f x) / h) ^ 2 ∂μ) ≤
      (4 / h ^ 2) * ∫ x in K, (f x) ^ 2 ∂μ := by
…