FiberAverageL2.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Square-integrable averages over probability fibers

These estimates justify the whole-fiber averages in the inverse coupling. The outer measure may be finite without being normalized.

def OAI.PolycyclicRecognition.normalizedRestriction line 27
Source documentation
Normalize the restriction to a region of positive finite mass.
```
def normalizedRestriction (m : Measure Y) (B : Set Y) : Measure Y :=
…
```
theorem OAI.PolycyclicRecognition.normalizedRestriction_probability line 32
Source documentation
A positive finite region defines a probability measure on its whole volume, rather than on a chosen representative point.
```
theorem normalizedRestriction_probability (m : Measure Y) {B : Set Y}
    (hB0 : m B ≠ 0) (hBtop : m B ≠ ∞) :
    IsProbabilityMeasure (normalizedRestriction m B) := by
…
```
Mentions: OAI.PolycyclicRecognition.normalizedRestriction

theorem OAI.PolycyclicRecognition.memLp_normalizedRestriction_product line 41

Source documentation

Normalizing one finite fiber preserves square integrability.

theorem memLp_normalizedRestriction_product (ν : Measure X) [SFinite ν]
    (m : Measure Y) [SFinite m] {B : Set Y} (hB0 : m B ≠ 0)
    {f : X × Y → W} (hf : MemLp f 2 (ν.prod (m.restrict B))) :
    MemLp f 2 (ν.prod (normalizedRestriction m B)) := by
…

Mentions: OAI.PolycyclicRecognition.normalizedRestriction

theorem OAI.PolycyclicRecognition.lintegral_normalizedRestriction_two line 51

Source documentation

Normalizing both averaging variables contributes exactly the inverse square of the region's mass.

theorem lintegral_normalizedRestriction_two (ν : Measure X) (m : Measure Y)
    {B : Set Y} (hB0 : m B ≠ 0) (f : X → Y → Y → ℝ≥0∞) :
    (∫⁻ x, ∫⁻ y, ∫⁻ z, f x y z ∂(normalizedRestriction m B)
      ∂(normalizedRestriction m B) ∂ν) =
      ((m B)⁻¹) ^ 2 * ∫⁻ x, ∫⁻ y in B, ∫⁻ z in B, f x y z ∂m ∂m ∂ν := by
…

Mentions: OAI.PolycyclicRecognition.normalizedRestriction

theorem OAI.PolycyclicRecognition.norm_integral_sq_le line 62

Source documentation

Jensen's square estimate for the norm of a Bochner average.

theorem norm_integral_sq_le (β : Measure Y) [IsProbabilityMeasure β]
    {f : Y → W} (hf : MemLp f 2 β) :
    ‖∫ y, f y ∂β‖ ^ 2 ≤ ∫ y, ‖f y‖ ^ 2 ∂β := by
…

theorem OAI.PolycyclicRecognition.enorm_integral_sq_le line 74

Source documentation

The nonnegative extended-real form of the square estimate, used with Tonelli when comparing whole fibers.

theorem enorm_integral_sq_le (β : Measure Y) [IsProbabilityMeasure β]
    {f : Y → W} (hf : MemLp f 2 β) :
    ‖∫ y, f y ∂β‖ₑ ^ 2 ≤ ∫⁻ y, ‖f y‖ₑ ^ 2 ∂β := by
…

theorem OAI.PolycyclicRecognition.memLp_fiberAverage line 85

Source documentation

A square-integrable function on a finite product has square-integrable fiber averages, with the expected contraction of the squared norm.

theorem memLp_fiberAverage (ν : Measure X) [IsFiniteMeasure ν]
    (β : Measure Y) [IsProbabilityMeasure β]
    {f : X × Y → W} (hf : MemLp f 2 (ν.prod β)) :
    MemLp (fun x => ∫ y, f (x, y) ∂β) 2 ν ∧
      (∫ x, ‖∫ y, f (x, y) ∂β‖ ^ 2 ∂ν) ≤
        ∫ q, ‖f q‖ ^ 2 ∂(ν.prod β) := by
…

theorem OAI.PolycyclicRecognition.norm_sub_integral_sq_le line 113

Source documentation

Comparing two averages by the mean squared difference over the whole product fiber. This is the estimate used before enlarging translated balls.

theorem norm_sub_integral_sq_le [CompleteSpace W] (β : Measure Y) [IsProbabilityMeasure β]
    {f g : Y → W} (hf : MemLp f 2 β) (hg : MemLp g 2 β) :
    ‖(∫ y, f y ∂β) - ∫ y, g y ∂β‖ ^ 2 ≤
      ∫ y, ∫ z, ‖f y - g z‖ ^ 2 ∂β ∂β := by
…

theorem OAI.PolycyclicRecognition.enorm_sub_integral_sq_le line 135

Source documentation

Extended-real version of the whole-product oscillation estimate.

theorem enorm_sub_integral_sq_le [CompleteSpace W]
    (β : Measure Y) [IsProbabilityMeasure β]
    {f g : Y → W} (hf : MemLp f 2 β) (hg : MemLp g 2 β) :
    ‖(∫ y, f y ∂β) - ∫ y, g y ∂β‖ₑ ^ 2 ≤
      ∫⁻ y, ∫⁻ z, ‖f y - g z‖ₑ ^ 2 ∂β ∂β := by
…

theorem OAI.PolycyclicRecognition.fiber_average_error_lintegral_le line 158

Source documentation

The integrated error of fiber averages is controlled by the integrated oscillation over the full product of the fibers.

theorem fiber_average_error_lintegral_le [CompleteSpace W]
    (ν : Measure X) [IsFiniteMeasure ν] (β : Measure Y) [IsProbabilityMeasure β]
    {f g : X × Y → W} (hf : MemLp f 2 (ν.prod β)) (hg : MemLp g 2 (ν.prod β)) :
    (∫⁻ x, ‖∫ y, f (x, y) - g (x, y) ∂β‖ₑ ^ 2 ∂ν) ≤
      ∫⁻ x, ∫⁻ y, ∫⁻ z, ‖f (x, y) - g (x, z)‖ₑ ^ 2 ∂β ∂β ∂ν := by
…