CircleWedgeCost.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual random wedge cost for circle coordinates

The random covectors are exactly the intrinsic differentials of the modified circle maps. Fixed-width integrability follows from the original L² differentials and the cutoff, just as in the real case.

theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_circleRepresentative line 21
Distinct definitions of this name: OAI/Analysis/CircleDomains/Probability/MeasurableArcIndex.lean:32 (same statement text; different proof or body). Qualify references as OAI.CircleDomainRigidity.FiniteTransfer.measurable_circleRepresentative@path.
def OAI.CircleDomainRigidity.FiniteTransfer.circleCutoffFamily line 27
def OAI.CircleDomainRigidity.FiniteTransfer.circleWedges line 32
theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoff_circle_wedges_integrable_and_eq_cost line 35

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_grid_for_actual_circle_wedges line 85

Source documentation

The actual reciprocal grid selection applies to periodic coordinates with their intrinsic L² differentials and bounded circle representatives.

theorem exists_grid_for_actual_circle_wedges
    {n : ℕ} {S : Type*} [Countable S] {G : Set (ℝ × ℝ)} (hG : IsOpen G)
    (f : Fin n → (ℝ × ℝ) → UnitAddCircle) (χ : (ℝ × ℝ) → ℝ)
    (hf : ∀ i, SmoothCircleOn (f i) G) (hmf : ∀ i, Measurable (f i))
    (hdf : ∀ i, Measurable (circleGradient (f i)))
    (hf2 : ∀ i, MemLp (circleGradient (f i)) 2 (volume.restrict G))
    (hχ : ContDiff ℝ ∞ χ) (hdχ : Measurable (planarGradient χ))
    (hχ2 : MemLp (planarGradient χ) 2 (volume.restrict G))
    (hχ0 : ∀ z, 0 ≤ χ z) (hχ1 : ∀ z, χ z ≤ 1)
    (F : Set S) (hF : F.Finite) (a b : Fin n → S → ℝ)
    (hwidth : ∀ i s, 0 ≤ b i s - a i s)
    (hwidth2 : ∀ i, Summable (fun s => (b i s - a i s) ^ 2))
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn, OAI.CircleDomainRigidity.FiniteTransfer.circleGradient, OAI.CircleDomainRigidity.FiniteTransfer.planarGradient