FiberIncrementBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Comparing whole fibers by bounded increments

Tonelli and the left-Haar change of variables turn a two-region oscillation integral into a bounded-parameter integral of the original increment errors. The translating center may depend on the section point.

theorem OAI.PolycyclicRecognition.lintegral_translate_le line 26

Source documentation

Enlarge a translated averaging region using its actual inclusion. The integrand needs no regularity for this step.

theorem lintegral_translate_le (m : Measure G) [m.IsMulLeftInvariant]
    (f : G → ℝ≥0∞) (q : G) {B C : Set G} (h : ∀ x ∈ B, q * x ∈ C) :
    (∫⁻ x in B, f (q * x) ∂m) ≤ ∫⁻ x in C, f x ∂m := by
…

theorem OAI.PolycyclicRecognition.fiber_increment_lintegral_le line 35

Source documentation

The substitution t = x₂⁻¹x₁ bounds whole-region oscillations by increments whose parameters lie in one fixed set.

theorem fiber_increment_lintegral_le
    (ν : Measure X) [SFinite ν] (m : Measure G) [SFinite m] [m.IsMulLeftInvariant]
    {B C T : Set G} (hB : MeasurableSet B)
    (hT : ∀ x₂ ∈ B, ∀ x₁ ∈ C, x₂⁻¹ * x₁ ∈ T)
    (f : X → G → G → ℝ≥0∞) (hf : Measurable (fun q : X × G × G => f q.1 q.2.1 q.2.2)) :
    (∫⁻ p, ∫⁻ x₁ in C, ∫⁻ x₂ in B, f p x₂ (x₂⁻¹ * x₁) ∂m ∂m ∂ν) ≤
      ∫⁻ t in T, ∫⁻ p, ∫⁻ x₂ in B, f p x₂ t ∂m ∂ν ∂m := by
…

theorem OAI.PolycyclicRecognition.fiber_translated_increment_lintegral_le line 78

Source documentation

The two-region estimate remains uniform when the first averaging region is translated by a center depending on the section point.

theorem fiber_translated_increment_lintegral_le
    (ν : Measure X) [SFinite ν] (m : Measure G) [SFinite m] [m.IsMulLeftInvariant]
    {B C T : Set G} (hB : MeasurableSet B)
    (hT : ∀ x₂ ∈ B, ∀ x₁ ∈ C, x₂⁻¹ * x₁ ∈ T)
    (q : X → G) (hC : ∀ p x, x ∈ B → q p * x ∈ C)
    (f : X → G → G → ℝ≥0∞) (hf : Measurable (fun a : X × G × G => f a.1 a.2.1 a.2.2)) :
    (∫⁻ p, ∫⁻ x₁ in B, ∫⁻ x₂ in B, f p x₂ (x₂⁻¹ * (q p * x₁)) ∂m ∂m ∂ν) ≤
      ∫⁻ t in T, ∫⁻ p, ∫⁻ x₂ in B, f p x₂ t ∂m ∂ν ∂m := by
…

theorem OAI.PolycyclicRecognition.fiber_translated_increment_uniform_le line 93

Source documentation

Uniform control on the compact increment region bounds the whole oscillation integral by the Haar mass of that region.

theorem fiber_translated_increment_uniform_le
    (ν : Measure X) [SFinite ν] (m : Measure G) [SFinite m] [m.IsMulLeftInvariant]
    {B C T : Set G} (hB : MeasurableSet B) (hTm : MeasurableSet T)
    (hT : ∀ x₂ ∈ B, ∀ x₁ ∈ C, x₂⁻¹ * x₁ ∈ T)
    (q : X → G) (hC : ∀ p x, x ∈ B → q p * x ∈ C)
    (f : X → G → G → ℝ≥0∞) (hf : Measurable (fun a : X × G × G => f a.1 a.2.1 a.2.2))
    {c : ℝ≥0∞} (hbound : ∀ t ∈ T, (∫⁻ p, ∫⁻ x₂ in B, f p x₂ t ∂m ∂ν) ≤ c) :
    (∫⁻ p, ∫⁻ x₁ in B, ∫⁻ x₂ in B, f p x₂ (x₂⁻¹ * (q p * x₁)) ∂m ∂m ∂ν) ≤
      c * m T := by
…