MaskedMetric.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common metric for coordinates on different masks

Only the actual masked covectors enter the wedge budget. Auxiliary smooth coordinates agree with them outside the retained core, so the resulting metric controls the sum of energies on the respective masks.

def OAI.CircleDomainRigidity.FiniteTransfer.maskedWedges line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy_eq_indicator_of_maskedGradient line 27

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_spherical_metric_for_masked_coordinates line 40

Source documentation

Small wedges of the actual masked differentials give one smooth metric for all masks, with the prescribed total energy.

theorem exists_spherical_metric_for_masked_coordinates
    {n : ℕ} {Ω Q K : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hK : IsClosed K) (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)))
    {ε : ℝ} (hbudget : (∫ z in Q \ K, 2 * maskedWedges M f z) < ε) :
    ∃ (R : ℝ) (g : (ℝ × ℝ) → PlanarMetric), 0 < R ∧ ContDiff ℝ ∞ g ∧
      (∀ z, (g z).PosDef) ∧
      (∀ᶠ z in 𝓝ˢ K, g z = sphericalMetricFactor z • 1) ∧
      (∀ z ∉ Metric.closedBall 0 R, g z = sphericalMetricFactor z • 1) ∧
      (∑ i : Fin n, ∫ z in (Q \ K) ∩ M i, gradientEnergy (f i) g z) < ε := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.maskedWedges, OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor, OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy