OriginalDomainMetric.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Charging the completed surface to the original domain

Inside every added disk the coordinate differential has rank at most one. Consequently the completed surface's wedge integral is bounded by the original-domain integral; no extension or integrability of the original coordinates in the missing disks is needed.

theorem OAI.CircleDomainRigidity.FiniteTransfer.coordinateWedges_nonneg line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.coordinateWedges_eq_zero line 27

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.integral_wedges_le_original line 48

Source documentation

The added rank-one pieces have no cost. Only the raw coordinates on G \ K enter the estimate.

theorem IsFilledCoordinateFamily.integral_wedges_le_original
    {I : Type*} [Fintype I] {n : ℕ} {D : I → Set (ℝ × ℝ)}
    {Ω Q K G : Set (ℝ × ℝ)} {v F : Fin n → (ℝ × ℝ) → ℝ}
    (hF : IsFilledCoordinateFamily D Ω v F) (hD : ∀ i, IsOpen (D i))
    (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hK : IsClosed K) (hG : MeasurableSet G) (hcover : Q ⊆ G ∪ ⋃ i, D i)
    (hv : IntegrableOn (fun z => 2 * coordinateWedges (natCoordinateFamily v) n z) (G \ K)) :
    (∫ z in Q \ K, 2 * coordinateWedges (natCoordinateFamily F) n z) ≤
      ∫ z in G \ K, 2 * coordinateWedges (natCoordinateFamily v) n z := by
…

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

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.exists_spherical_metric_of_original_cost line 83

Source documentation

The original-domain cost produces a metric retaining the spherical background near the closed core and near infinity.

theorem IsFilledCoordinateFamily.exists_spherical_metric_of_original_cost
    {I : Type*} [Fintype I] {n : ℕ} {D : I → Set (ℝ × ℝ)}
    {Ω Q K G : Set (ℝ × ℝ)} {v F : Fin n → (ℝ × ℝ) → ℝ}
    (hF : IsFilledCoordinateFamily D Ω v F) (hD : ∀ i, IsOpen (D i))
    (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hK : IsClosed K) (hG : MeasurableSet G) (hcover : Q ⊆ G ∪ ⋃ i, D i)
    (hv : IntegrableOn (fun z => 2 * coordinateWedges (natCoordinateFamily v) n z) (G \ K))
    {ε : ℝ} (hε : (∫ z in G \ K, 2 * coordinateWedges (natCoordinateFamily v) n 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) ∧
…

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