UpperPairs.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual finite wedge sum and its pair indexing

Each unordered coordinate pair occurs exactly once. This identifies the spatial cost selected by the random-grid argument with the wedge sum of the actual cutoff staircase differentials.

abbrev OAI.CircleDomainRigidity.FiniteTransfer.UpperPairs line 20
def OAI.CircleDomainRigidity.FiniteTransfer.upperPair line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.upperPair_ne line 25
theorem OAI.CircleDomainRigidity.FiniteTransfer.upperPair_covers line 30
theorem OAI.CircleDomainRigidity.FiniteTransfer.covectorWedges_eq_sum_upperPairs line 39
theorem OAI.CircleDomainRigidity.FiniteTransfer.coordinateWedges_eq_sum_upperPairs line 49

theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_cutoff_wedges_eq_staircaseWedgeCost line 65

Source documentation

Exact identity with the random-grid cost; the integrability hypotheses concern only the finitely many selected spatial pair costs.

theorem integral_cutoff_wedges_eq_staircaseWedgeCost
    {μ : Measure (ℝ × ℝ)} {n : ℕ}
    (u : Fin n → (ℝ × ℝ) → ℝ) (χ : (ℝ × ℝ) → ℝ)
    {h δ : ℝ} (hh : 0 < h) (hδ : 0 < δ) (hδh : δ < h / 4) (θ : Fin n → ℝ)
    (hd : ∀ᵐ z ∂μ, DifferentiableAt ℝ χ z ∧ ∀ i, DifferentiableAt ℝ (u i) z)
    (hi : ∀ p : UpperPairs n, Integrable (fun z => |planarWedge
      (staircaseCovector h δ (χ z) (θ (upperPair p).1) (u (upperPair p).1 z)
        (planarGradient (u (upperPair p).1) z) (planarGradient χ z))
      (staircaseCovector h δ (χ z) (θ (upperPair p).2) (u (upperPair p).2 z)
        (planarGradient (u (upperPair p).2) z) (planarGradient χ z))|) μ) :
    (∫ z, coordinateWedges (natCoordinateFamily
      (fun i => cutoffStaircase (u i) χ (shiftedStaircase h δ (θ i)))) n z ∂μ) =
…