ExpectedWedges.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

+# Expected wedges for a finite family of actual random staircases

The product space has one uniform shift per coordinate. Distinct labels have the two-shift law used in the analytic mean calculation.

def OAI.CircleDomainRigidity.FiniteTransfer.staircaseCovector line 17
theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_staircaseCovector line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.expected_grid_pair_wedge_le line 32

theorem OAI.CircleDomainRigidity.FiniteTransfer.expected_integrated_grid_pair_wedge_le line 57

Source documentation

Fubini turns the pointwise mean estimate into the spatial wedge estimate. Joint integrability is exposed so this can be used both on compact smooth pieces and on exhausted finite-energy regions.

theorem expected_integrated_grid_pair_wedge_le
    {X : Type*} [MeasurableSpace X] {μ : Measure X} [SFinite μ]
    {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (u v c : X → ℝ × ℝ) (x y χ : X → ℝ) {h δ : ℝ}
    (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4)
    (hχ0 : ∀ z, 0 ≤ χ z) (hχ1 : ∀ z, χ z ≤ 1)
    (hjoint : 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))|)
      (((shiftLaw h).prod (shiftLaw h)).prod μ))
    (hbound : Integrable (fun z => |planarWedge (u z) (v z)| +
…

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