MaskedCircleCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual masked circle cost away from the retained core

Mask boundaries lie inside the core. On its complement every active mask is locally present, so the circle cutoff formula holds there. This identifies the masked random cost with the actual spatial wedge sum and proves integrability from each coordinate's own masked L² norm.

theorem OAI.CircleDomainRigidity.FiniteTransfer.masked_circle_cutoff_wedges_integrable_and_eq_cost line 22

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_grid_for_actual_masked_circle_wedges line 90

Source documentation

Grid selection for the actual masked circle cutoff, with finite terminal indices and an arbitrarily late good width.

theorem exists_grid_for_actual_masked_circle_wedges
    {n : ℕ} {S : Type*} [Countable S] {G K : Set (ℝ × ℝ)}
    (hG : IsOpen G) (hK : MeasurableSet K)
    (M : Fin n → Set (ℝ × ℝ)) (hM : ∀ i, MeasurableSet (M i))
    (hboundary : ∀ i, frontier (M i) ⊆ K)
    (f : Fin n → (ℝ × ℝ) → UnitAddCircle) (χ : (ℝ × ℝ) → ℝ)
    (hf : ∀ i, SmoothCircleOn (f i) (G ∩ interior (M i)))
    (hmf : ∀ i, Measurable (f i)) (hdf : ∀ i, Measurable (circleGradient (f i)))
    (hf2 : ∀ i, MemLp (circleGradient (f i)) 2
      ((volume.restrict (G \ K)).restrict (M i)))
    (hχ : ContDiff ℝ ∞ χ) (hdχ : Measurable (planarGradient χ))
    (hχ2 : MemLp (planarGradient χ) 2 (volume.restrict (G \ K)))
…

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