StaircaseWedge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Expected wedge of actual staircase coordinates

This instantiates the averaging bound with the constructed smooth staircase family. After division by h², the error is proportional to h, uniformly in the transition width.

theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_shiftedStaircase_value line 21

theorem OAI.CircleDomainRigidity.FiniteTransfer.average_staircase_wedge_le line 30

Source documentation

The finite-transfer wedge bound for two independently shifted actual staircases, prior to summing over coordinate pairs and domain points.

theorem average_staircase_wedge_le (u v c : ℝ × ℝ) (x y : ℝ)
    {h δ χ : ℝ} (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4)
    (hχ0 : 0 ≤ χ) (hχ1 : χ ≤ 1) :
    (∫ z in Icc 0 h ×ˢ Icc 0 h,
      |planarWedge
        (((1 - χ) + χ * deriv (shiftedStaircase h δ z.1) x) • u +
          (shiftedStaircase h δ z.1 x - x) • c)
        (((1 - χ) + χ * deriv (shiftedStaircase h δ z.2) y) • v +
          (shiftedStaircase h δ z.2 y - y) • c)| ∂volume.prod volume) / h ^ 2 ≤
      |planarWedge u v| + h * (|planarWedge u c| + |planarWedge c v|) := by
…

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