WedgeIntegrability.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Joint integrability of the actual random wedge

Tonelli and the pointwise expected-wedge bound prove joint integrability. Thus applying Fubini to the random staircase construction needs only measurable input fields and the original integrable wedge majorant.

theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_abs_planarWedge_of_memLp line 21
Source documentation
Finite squared norms of the original planar covectors make their absolute wedge product integrable by Hölder's inequality.
```
theorem integrable_abs_planarWedge_of_memLp
    {X : Type*} [MeasurableSpace X] {μ : Measure X} {u v : X → ℝ × ℝ}
    (hu : MemLp u 2 μ) (hv : MemLp v 2 μ) :
    Integrable (fun z => |planarWedge (u z) (v z)|) μ := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge
theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_nonnegative_prod_of_inner_bound line 33
theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_shiftLaw_pair_of_continuous line 56
Source documentation
Every continuous two-shift integrand is integrable for the actual compactly supported product shift law.
```
theorem integrable_shiftLaw_pair_of_continuous {h : ℝ} (hh : 0 < h)
    {f : ℝ × ℝ → ℝ} (hf : Continuous f) :
    Integrable f ((shiftLaw h).prod (shiftLaw h)) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.shiftLaw
theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_staircaseCovector line 65

theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_staircase_pair_density line 82

Source documentation

Joint integrability follows from the original wedge and cutoff terms; it is not assumed before interchanging the spatial and shift integrals.

theorem integrable_staircase_pair_density
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
    (u v c : X → ℝ × ℝ) (x y χ : X → ℝ)
    (hu : Measurable u) (hv : Measurable v) (hc : Measurable c)
    (hx : Measurable x) (hy : Measurable y) (hχ : Measurable χ)
    {h δ : ℝ} (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4)
    (hχ0 : ∀ z, 0 ≤ χ z) (hχ1 : ∀ z, χ z ≤ 1)
    (hbound : Integrable (fun z => |planarWedge (u z) (v z)| +
      h * (|planarWedge (u z) (c z)| + |planarWedge (c z) (v z)|)) μ) :
    Integrable (fun p : (ℝ × ℝ) × X => |planarWedge
      (staircaseCovector h δ (χ p.2) p.1.1 (x p.2) (u p.2) (c p.2))
      (staircaseCovector h δ (χ p.2) p.1.2 (y p.2) (v p.2) (c p.2))|)
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarWedge, OAI.CircleDomainRigidity.FiniteTransfer.staircaseCovector