Translation.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.integral_increment_eq_boundary line 12

Source documentation

Integrating a measure-preserving increment over a common core leaves only boundary terms.

theorem integral_increment_eq_boundary {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {f : X → X} (hf : MeasurePreserving f μ μ)
    (he : MeasurableEmbedding f) {K A : Set X} (hA : MeasurableSet A)
    (hAK : A ⊆ K) (hBK : f '' A ⊆ K) {g : X → ℝ} (hg : IntegrableOn g K μ) :
    (∫ x in A, (g (f x) - g x) ∂μ) =
      (∫ x in K \ A, g x ∂μ) - ∫ x in K \ (f '' A), g x ∂μ := by
…

theorem OAI.Problem358.abs_integral_increment_le_boundary line 28

Source documentation

A bounded function has a small mean increment whenever the common core loses little mass.

theorem abs_integral_increment_le_boundary {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {f : X → X} (hf : MeasurePreserving f μ μ)
    (he : MeasurableEmbedding f) {K A : Set X} (hKfin : μ K ≠ ⊤)
    (hA : MeasurableSet A) (hAK : A ⊆ K) (hBK : f '' A ⊆ K)
    {g : X → ℝ} (hg : IntegrableOn g K μ) {L : ℝ}
    (hbound : ∀ x ∈ K, |g x| ≤ L) :
    |∫ x in A, (g (f x) - g x) ∂μ| ≤ 2 * L * μ.real (K \ A) := by
…

theorem OAI.Problem358.integral_error_sq_le_boundary line 59

Source documentation

A one-sided bounded error inherits an integrated square bound from boundary mass.

theorem integral_error_sq_le_boundary {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {f : X → X} (hf : MeasurePreserving f μ μ)
    (he : MeasurableEmbedding f) {K A : Set X} (hKfin : μ K ≠ ⊤)
    (hA : MeasurableSet A) (hAK : A ⊆ K) (hBK : f '' A ⊆ K)
    {g δ : X → ℝ} (hg : IntegrableOn g K μ)
    {L : ℝ} (hL : 0 ≤ L) (hbound : ∀ x ∈ K, |g x| ≤ L)
    (hδint : IntegrableOn (fun x => δ x ^ 2) A μ)
    (hδ : ∀ᵐ x ∂μ.restrict A,
      0 ≤ δ x ∧ δ x ≤ g (f x) - g x ∧ g (f x) - g x ≤ 2 * L) :
    (∫ x in A, δ x ^ 2 ∂μ) ≤ 4 * L ^ 2 * μ.real (K \ A) := by
…

theorem OAI.Problem358.slice_translation_identity line 95

Source documentation

Translation cancellation on a one-dimensional slice.

theorem slice_translation_identity {g : ℝ → ℝ} {a b h : ℝ}
    (hh : 0 ≤ h) (hhab : h ≤ b - a)
    (hg : IntervalIntegrable g volume a b) :
    (∫ t in a..b-h, (g (t+h) - g t)) =
      (∫ t in b-h..b, g t) - ∫ t in a..a+h, g t := by
…

theorem OAI.Problem358.slice_translation_le line 112

Source documentation

Bounded derivatives have shift discrepancy at most twice the boundary strip size.

theorem slice_translation_le {g : ℝ → ℝ} {a b h L : ℝ}
    (hh : 0 ≤ h) (hhab : h ≤ b-a)
    (hg : IntervalIntegrable g volume a b)
    (hbound : ∀ t ∈ Icc a b, |g t| ≤ L) :
    (∫ t in a..b-h, (g (t+h) - g t)) ≤ 2*L*h := by
…

theorem OAI.Problem358.slice_error_sq_le line 135

Source documentation

The one-dimensional squared finite-difference error estimate used on convex slices.

theorem slice_error_sq_le {g δ : ℝ → ℝ} {a b h L : ℝ}
    (hh : 0 ≤ h) (hhab : h ≤ b-a) (hL : 0 ≤ L)
    (hg : IntervalIntegrable g volume a b)
    (hbound : ∀ t ∈ Icc a b, |g t| ≤ L)
    (hδ : ∀ t ∈ Icc a (b-h), 0 ≤ δ t ∧ δ t ≤ g (t+h)-g t)
    (hδint : IntervalIntegrable (fun t => δ t ^ 2) volume a (b-h)) :
    (∫ t in a..b-h, δ t ^ 2) ≤ 4*L^2*h := by
…

theorem OAI.Problem358.slice_error_sq_integrable line 168

Source documentation

Bounded measurable slice errors have an integrable square.

theorem slice_error_sq_integrable {δ : ℝ → ℝ} {a b L : ℝ}
    (hab : a ≤ b) (hL : 0 ≤ L) (hδmeas : Measurable δ)
    (hδ : ∀ t ∈ Icc a b, 0 ≤ δ t ∧ δ t ≤ 2*L) :
    IntervalIntegrable (fun t => δ t ^ 2) volume a b := by
…

theorem OAI.Problem358.slice_error_sq_le_of_measurable line 184

Source documentation

Measurable form of the squared finite-difference error estimate.

theorem slice_error_sq_le_of_measurable {g δ : ℝ → ℝ} {a b h L : ℝ}
    (hh : 0 ≤ h) (hhab : h ≤ b-a) (hL : 0 ≤ L)
    (hg : IntervalIntegrable g volume a b)
    (hbound : ∀ t ∈ Icc a b, |g t| ≤ L)
    (hδmeas : Measurable δ)
    (hδ : ∀ t ∈ Icc a (b-h), 0 ≤ δ t ∧ δ t ≤ g (t+h)-g t) :
    (∫ t in a..b-h, δ t ^ 2) ≤ 4*L^2*h := by
…

theorem OAI.Problem358.slice_error_sq_integrable_ae line 202

Source documentation

Almost-everywhere bounds suffice to establish square integrability on a slice.

theorem slice_error_sq_integrable_ae {δ : ℝ → ℝ} {a b L : ℝ}
    (hab : a ≤ b) (hL : 0 ≤ L)
    (hδmeas : AEStronglyMeasurable δ (volume.restrict (Icc a b)))
    (hδ : ∀ᵐ t ∂volume.restrict (Icc a b), 0 ≤ δ t ∧ δ t ≤ 2*L) :
    IntervalIntegrable (fun t => δ t ^ 2) volume a b := by
…

theorem OAI.Problem358.slice_error_sq_le_ae line 214

Source documentation

The quotient error estimate tolerates the null exceptional set of derivative existence.

theorem slice_error_sq_le_ae {g δ : ℝ → ℝ} {a b h L : ℝ}
    (hh : 0 ≤ h) (hhab : h ≤ b-a) (hL : 0 ≤ L)
    (hg : IntervalIntegrable g volume a b)
    (hbound : ∀ t ∈ Icc a b, |g t| ≤ L)
    (hδmeas : AEStronglyMeasurable δ (volume.restrict (Icc a (b-h))))
    (hδ : ∀ᵐ t ∂volume.restrict (Icc a (b-h)),
      0 ≤ δ t ∧ δ t ≤ g (t+h)-g t) :
    (∫ t in a..b-h, δ t ^ 2) ≤ 4*L^2*h := by
…

theorem OAI.Problem358.intervalIntegrable_of_measurable_abs_bound line 262
theorem OAI.Problem358.intervalIntegrable_deriv_of_lipschitz line 273
Source documentation
A globally Lipschitz real function has an interval-integrable derivative, including at the points where deriv is defined to be zero.
```
theorem intervalIntegrable_deriv_of_lipschitz {u : ℝ → ℝ} {L : ℝ≥0}
    (hu : LipschitzWith L u) (a b : ℝ) :
    IntervalIntegrable (deriv u) volume a b := by
…
```
theorem OAI.Problem358.abs_forwardQuotient_le_of_lipschitz line 281
Source documentation
Forward quotients of a Lipschitz function have the same bound.
```
theorem abs_forwardQuotient_le_of_lipschitz {u : ℝ → ℝ} {L : ℝ≥0}
    (hu : LipschitzWith L u) {h : ℝ} (hh : 0 < h) (x : ℝ) :
    |forwardQuotient u h x| ≤ L := by
…
```
Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.intervalIntegrable_forwardQuotient_error_sq line 291

Source documentation

Squared finite-difference errors are integrable without any continuity assumption on the derivative.

theorem intervalIntegrable_forwardQuotient_error_sq {u : ℝ → ℝ} {L : ℝ≥0}
    (hu : LipschitzWith L u) {h : ℝ} (hh : 0 < h) (a b : ℝ) :
    IntervalIntegrable (fun x => (forwardQuotient u h x - deriv u x) ^ 2) volume a b := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.ae_convex_forwardQuotient_error_sq_le line 314

Source documentation

Convex quotient control holds almost everywhere for globally convex Lipschitz functions, because translation preserves null sets.

theorem ae_convex_forwardQuotient_error_sq_le {u : ℝ → ℝ} {L : ℝ≥0}
    (hu : ConvexOn ℝ univ u) (hLip : LipschitzWith L u) {h : ℝ} (hh : 0 < h) :
    ∀ᵐ x : ℝ, (forwardQuotient u h x - deriv u x) ^ 2 ≤
      2 * (L : ℝ) * (deriv u (x + h) - deriv u x) := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.convex_slice_quotient_error_sq_le line 329

Source documentation

The squared quotient error integrated on the allowed part of a slice is bounded by 4 L² h, with no everywhere-differentiability assumption.

theorem convex_slice_quotient_error_sq_le {u : ℝ → ℝ} {L : ℝ≥0}
    (hu : ConvexOn ℝ univ u) (hLip : LipschitzWith L u)
    {a b h : ℝ} (hh : 0 < h) (hhab : h ≤ b - a) :
    (∫ x in a..b-h, (forwardQuotient u h x - deriv u x) ^ 2) ≤
      4 * (L : ℝ) ^ 2 * h := by
…

Mentions: OAI.Problem358.forwardQuotient

theorem OAI.Problem358.sq_deriv_sub_le_of_lipschitz line 357

Source documentation

The difference of derivatives of two Lipschitz real functions is bounded pointwise, including the default values at nondifferentiability points.

theorem sq_deriv_sub_le_of_lipschitz {u v : ℝ → ℝ} {L₀ L₁ : ℝ≥0}
    (hu : LipschitzWith L₀ u) (hv : LipschitzWith L₁ v) (x : ℝ) :
    (deriv u x - deriv v x) ^ 2 ≤ ((L₀ : ℝ) + (L₁ : ℝ)) ^ 2 := by
…

theorem OAI.Problem358.intervalIntegrable_sq_deriv_sub_of_lipschitz line 370

Source documentation

Squared derivative differences are interval-integrable.

theorem intervalIntegrable_sq_deriv_sub_of_lipschitz {u v : ℝ → ℝ} {L₀ L₁ : ℝ≥0}
    (hu : LipschitzWith L₀ u) (hv : LipschitzWith L₁ v) (a b : ℝ) :
    IntervalIntegrable (fun x => (deriv u x - deriv v x) ^ 2) volume a b := by
…

theorem OAI.Problem358.integral_sq_deriv_sub_le_of_lipschitz line 382

Source documentation

Boundary-strip estimate for squared derivative differences.

theorem integral_sq_deriv_sub_le_of_lipschitz {u v : ℝ → ℝ} {L₀ L₁ : ℝ≥0}
    (hu : LipschitzWith L₀ u) (hv : LipschitzWith L₁ v) {a b : ℝ} (hab : a ≤ b) :
    (∫ x in a..b, (deriv u x - deriv v x) ^ 2) ≤
      ((L₀ : ℝ) + (L₁ : ℝ)) ^ 2 * (b - a) := by
…