MaskedCoordinates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Smooth auxiliary coordinates for closed masks

The mask boundaries lie strictly inside the retained core. Smooth extensions therefore realize the masked coordinate differentials exactly on the region where the metric is changed. Their arbitrary values in the core never enter the tail energy estimate.

def OAI.CircleDomainRigidity.FiniteTransfer.maskedGradient line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_masked_coordinate line 27
Source documentation
Closed masks with boundaries in the interior of the retained core admit globally smooth auxiliary coordinates with the exact masked covectors everywhere outside that core in the completed piece.
```
theorem exists_smooth_masked_coordinate
    {Ω Q K M : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hM : IsClosed M) (hboundary : frontier M ⊆ interior K)
    {f : (ℝ × ℝ) → ℝ} (hf : ContDiffOn ℝ ∞ f (Ω ∩ interior M)) :
    ∃ F : (ℝ × ℝ) → ℝ, ContDiff ℝ ∞ F ∧
      ∀ z ∈ Q \ K, planarGradient F z = maskedGradient M f z := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient, OAI.CircleDomainRigidity.FiniteTransfer.maskedGradient

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_masked_family line 57

Source documentation

A finite family of masked coordinates can be handled simultaneously. The equality is an equality of actual planar covectors.

theorem exists_smooth_masked_family
    {n : ℕ} {Ω Q K : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (M : Fin n → Set (ℝ × ℝ)) (hM : ∀ i, IsClosed (M i))
    (hboundary : ∀ i, frontier (M i) ⊆ interior K)
    (f : Fin n → (ℝ × ℝ) → ℝ) (hf : ∀ i, ContDiffOn ℝ ∞ (f i) (Ω ∩ interior (M i))) :
    ∃ F : Fin n → (ℝ × ℝ) → ℝ, (∀ i, ContDiff ℝ ∞ (F i)) ∧
      ∀ i z, z ∈ Q \ K → planarGradient (F i) z = maskedGradient (M i) (f i) z := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient, OAI.CircleDomainRigidity.FiniteTransfer.maskedGradient