ConformalMetric.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Restoring the spherical metric factor

In two dimensions positive scalar rescaling leaves the full Dirichlet energy density unchanged. Thus a compactly supported metric modification in a planar chart can retain the original spherical factor both near the core and outside a compact set.

theorem OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy_pos_smul line 21
def OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor line 34
theorem OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor_pos line 37
theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiff_sphericalMetricFactor line 41

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_supported_spherical_metric_for_coordinates line 50

Source documentation

Small energy for the actual spherical background factor, with exact agreement near an arbitrary closed retained core and near infinity.

theorem exists_supported_spherical_metric_for_coordinates
    (f : ℕ → (ℝ × ℝ) → ℝ) (n : ℕ) {Ω Q K : Set (ℝ × ℝ)}
    (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hf : ∀ i, ContDiffOn ℝ ∞ (f i) Ω) (hK : IsClosed K) {ε : ℝ}
    (hε : (∫ z in Q \ K, 2 * coordinateWedges f n z) < ε) :
    ∃ (R : ℝ) (g : (ℝ × ℝ) → PlanarMetric), 0 < R ∧ ContDiff ℝ ∞ g ∧
      (∀ z, (g z).PosDef) ∧
      (∀ᶠ z in 𝓝ˢ K, g z = sphericalMetricFactor z • 1) ∧
      (∀ z ∉ closedBall 0 R, g z = sphericalMetricFactor z • 1) ∧
      (∫ z in Q \ K, matrixEnergy (coordinateGram f n z) (g z)) < ε := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.coordinateWedges, OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor, OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy, OAI.CircleDomainRigidity.FiniteTransfer.coordinateGram