SlicedIntegral.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

From almost-everywhere line estimates to planar estimates, including the area-preserving coordinates of a fixed reference slope.

theorem OAI.LipschitzHilbert.integral_le_of_slices line 20

Source documentation

For a nonnegative measurable integrand, integrable slices and a common integrable bound on their integrals prove the full product estimate.

theorem integral_le_of_slices (μ : Measure α) (ν : Measure β)
    [SFinite μ] [SFinite ν] (f g : α × β → ℝ) {C : ℝ}
    (hfmeas : AEStronglyMeasurable f (μ.prod ν)) (hf0 : ∀ z, 0 ≤ f z)
    (hg : Integrable g (μ.prod ν))
    (hfslice : ∀ᵐ y ∂ν, Integrable (fun x => f (x, y)) μ)
    (hbound : ∀ᵐ y ∂ν, (∫ x, f (x, y) ∂μ) ≤ C * ∫ x, g (x, y) ∂μ) :
    Integrable f (μ.prod ν) ∧
      (∫ z, f z ∂μ.prod ν) ≤ C * ∫ z, g z ∂μ.prod ν := by
…

def OAI.LipschitzHilbert.slopeShear line 42
Source documentation
The coordinate map (x,y) ↦ (x,y+s*x), with its explicit inverse.
```
def slopeShear (s : ℝ) : ℝ × ℝ ≃ᵐ ℝ × ℝ where
…
```
theorem OAI.LipschitzHilbert.slopeShear_measurePreserving line 50
theorem OAI.LipschitzHilbert.integral_slopeShear line 57

theorem OAI.LipschitzHilbert.integral_le_of_slope_slices line 63

Source documentation

The slice argument applies in the reference-line coordinates without requiring a jointly measurable family of auxiliary prediction functions.

theorem integral_le_of_slope_slices (s : ℝ) (f g : ℝ × ℝ → ℝ) {C : ℝ}
    (hfmeas : AEStronglyMeasurable f (volume.prod volume)) (hf0 : ∀ z, 0 ≤ f z)
    (hg : Integrable g (volume.prod volume))
    (hfslice : ∀ᵐ y ∂volume, Integrable (fun x => f (x, y + s * x)) volume)
    (hbound : ∀ᵐ y ∂volume,
      (∫ x, f (x, y + s * x)) ≤ C * ∫ x, g (x, y + s * x)) :
    Integrable f (volume.prod volume) ∧
      (∫ z, f z ∂volume.prod volume) ≤ C * ∫ z, g z ∂volume.prod volume := by
…