MaskedCorePreparation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Regular cores for the masked circle data

The original L² bounds on the separate masks make the actual masked wedge sum integrable. A regular retained core contains all mask boundaries and leaves an arbitrarily small tail. The original cutoff construction then supplies the compactly supported smooth interpolation.

theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_maskedCircleWedges_of_memLp line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.maskedCircleWedges_nonneg line 33

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_regular_masked_core_and_cutoff line 41

Source documentation

The core is constructed from the original masked energy. Its regularity uses only the previously identified scalar Sard input.

theorem exists_regular_masked_core_and_cutoff
    (hsard : SmoothPlanarSard) {G K₀ : Set (ℝ × ℝ)}
    (hG : IsOpen G) (hGc : IsCompact Gᶜ) (hK₀ : IsClosed K₀) (hK₀G : K₀ ⊆ G)
    {n : ℕ} (M : Fin n → Set (ℝ × ℝ)) (hM : ∀ i, MeasurableSet (M i))
    (hboundaryG : ∀ i, frontier (M i) ⊆ G)
    (f : Fin n → (ℝ × ℝ) → UnitAddCircle)
    (hf : ∀ i, MemLp (circleGradient (f i)) 2 ((volume.restrict G).restrict (M i)))
    {η : ℝ} (hη : 0 < η) :
    ∃ (ψ : (ℝ × ℝ) → ℝ) (t : ℝ) (K : Set (ℝ × ℝ)) (χ : (ℝ × ℝ) → ℝ),
      ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧ t ∈ Set.Ioo 0 1 ∧
      (∀ z, ψ z = t → fderiv ℝ ψ z ≠ 0) ∧ K = {z | ψ z ≤ t} ∧
      IsClosed K ∧ K₀ ⊆ interior K ∧ K ⊆ G ∧ IsCompact (closure Kᶜ) ∧
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.FiniteTransfer.circleGradient