MaskedCircleMetric.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

One metric for masked periodic coordinates

The actual intrinsic differentials of the circle coordinates are used throughout. Mask boundaries lie inside the retained core, so the masked covectors extend smoothly across the portion on which the metric changes. Their pairwise wedge budget controls the sum of energies on the masks.

def OAI.CircleDomainRigidity.FiniteTransfer.natCovectorFamily line 21
def OAI.CircleDomainRigidity.FiniteTransfer.maskedCircleWedges line 24
theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_natCovectorFamily line 30
theorem OAI.CircleDomainRigidity.FiniteTransfer.fieldWedges_eq_sum_upperPairs line 39
theorem OAI.CircleDomainRigidity.FiniteTransfer.fieldEnergy_indicator line 51

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_spherical_metric_for_masked_circles line 60

Source documentation

This is the masked metric step for genuine circle-valued coordinates; no globally defined scalar potentials are assumed.

theorem exists_spherical_metric_for_masked_circles
    {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 → (ℝ × ℝ) → UnitAddCircle)
    (hf : ∀ i, SmoothCircleOn (f i) (Ω ∩ interior (M i)))
    {ε : ℝ} (hbudget : (∫ z in Q \ K, 2 * maskedCircleWedges 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, fieldEnergy (circleGradient (f i)) g z) < ε := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.SmoothCircleOn, OAI.CircleDomainRigidity.FiniteTransfer.maskedCircleWedges, OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor, OAI.CircleDomainRigidity.FiniteTransfer.fieldEnergy, OAI.CircleDomainRigidity.FiniteTransfer.circleGradient