FilledMetric.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Passing from filled coordinates to a small-energy metric

The actual pointwise wedge inequality for the patched coordinates passes through the integral and then through metric selection. Only smoothness near the compact completed piece is used.

def OAI.CircleDomainRigidity.FiniteTransfer.natCoordinateFamily line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_natCoordinateFamily line 24
theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_coordinateWedges line 33
theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.coordinateWedges_le line 48

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.exists_small_energy_metric line 70

Source documentation

The completed coordinates admit an actual smooth positive definite metric retaining the original metric near the core and satisfying the same strict wedge-derived energy budget.

theorem IsFilledCoordinateFamily.exists_small_energy_metric
    {I : Type*} [Fintype I] {n : ℕ} {D : I → Set (ℝ × ℝ)}
    {Ω Q K U : Set (ℝ × ℝ)} {v F : Fin n → (ℝ × ℝ) → ℝ}
    (hF : IsFilledCoordinateFamily D Ω v F) (hD : ∀ i, IsOpen (D i))
    (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U)
    (hv : IntegrableOn (fun z => 2 * coordinateWedges (natCoordinateFamily v) n z) (Q \ K))
    {ε : ℝ} (hε : (∫ z in Q \ K, 2 * coordinateWedges (natCoordinateFamily v) n z) < ε) :
    ∃ (τ : ℝ) (N : Set (ℝ × ℝ)) (g : (ℝ × ℝ) → PlanarMetric),
      0 < τ ∧ IsOpen N ∧ K ⊆ N ∧ N ⊆ U ∧ ContDiff ℝ ∞ g ∧
      (∀ z, (g z).PosDef) ∧ (∀ᶠ z in 𝓝ˢ K, g z = 1) ∧
      (∀ z ∈ Q \ N, g z = coordinateGram (natCoordinateFamily F) n z + τ • 1) ∧
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily, OAI.CircleDomainRigidity.FiniteTransfer.coordinateWedges, OAI.CircleDomainRigidity.FiniteTransfer.natCoordinateFamily, OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.coordinateGram