CircleCutoffFillings.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Filling the actual descended circle cutoff

The collar functions are genuine local lifts of the original circle coordinates. On the one-plateau of the cutoff their staircases project to the actual modified maps. Smooth rank-one filling therefore applies to those maps, rather than to a separately specified surrogate.

theorem OAI.CircleDomainRigidity.FiniteTransfer.eventually_fill_actual_circle_cutoff line 21

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.eventuallyEq_original_on_core line 58

Source documentation

The actual filling agrees with the original circle coordinates on a full neighborhood of every retained closed core avoiding the disks.

theorem IsFilledCircleFamily.eventuallyEq_original_on_core
    {I L : Type*} [Fintype I] [Fintype L]
    {D : I → Set (ℝ × ℝ)} {Ω K : Set (ℝ × ℝ)}
    (hD : ∀ i, IsOpen (D i)) (hKD : ∀ x ∈ K, ∀ i, x ∉ D i)
    (f : L → (ℝ × ℝ) → UnitAddCircle) (χ : (ℝ × ℝ) → ℝ)
    (P : L → ℝ → ℝ) (hχzero : ∀ᶠ x in 𝓝ˢ K, χ x = 0)
    {F : L → (ℝ × ℝ) → UnitAddCircle}
    (hF : IsFilledCircleFamily D Ω (fun l => circleCutoff (f l) χ (P l)) F) :
    ∀ᶠ x in 𝓝ˢ K, ∀ l, F l x = f l x := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily, OAI.CircleDomainRigidity.FiniteTransfer.circleCutoff