CoordinateEstimates.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate energies on the completed surface

The metric trace estimate controls the sum of the actual scalar coordinate energies. Exact agreement near the retained core then gives localized estimates against the original domain, even though the original coordinates need not extend into the filled holes.

def OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy_nonneg line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy_spherical line 30
theorem OAI.CircleDomainRigidity.FiniteTransfer.coordinateGram_energy_eq_sum line 38
theorem OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy_le_coordinateGram line 44
theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_matrixEnergy_local line 51
theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_gradientEnergy line 68
theorem OAI.CircleDomainRigidity.FiniteTransfer.integrableOn_gradientEnergy line 96
theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_gradientEnergy_spherical_of_memLp line 104

theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_coordinateGram_eq_sum line 118

Source documentation

Integrating the trace really gives the sum of all transferred coordinate energies.

theorem integral_coordinateGram_eq_sum
    {Ω Q K : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (f : ℕ → (ℝ × ℝ) → ℝ) (hf : ∀ i, ContDiffOn ℝ ∞ (f i) Ω) (n : ℕ)
    {g : (ℝ × ℝ) → PlanarMetric} (hg : Continuous g) (hPD : ∀ z, (g z).PosDef) :
    (∫ z in Q \ K, matrixEnergy (coordinateGram f n z) (g z)) =
      ∑ i ∈ range n, ∫ z in Q \ K, gradientEnergy (f i) g z := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy, OAI.CircleDomainRigidity.FiniteTransfer.coordinateGram, OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy

theorem OAI.CircleDomainRigidity.FiniteTransfer.localized_energy_lt_source line 130

Source documentation

Compare localized energy to the original domain, without evaluating or integrating an original coordinate in the added holes.

theorem localized_energy_lt_source
    {X : Type*} [MeasurableSpace X] {μ : Measure X}
    {Q G K E : Set X} (hQ : MeasurableSet Q) (hG : MeasurableSet G)
    (hK : MeasurableSet K) (hE : MeasurableSet E) (hEK : E ⊆ K)
    (hQKG : Q ∩ K ⊆ G) {f u T : X → ℝ}
    (hf : IntegrableOn f Q μ) (hu : IntegrableOn u G μ)
    (hT : IntegrableOn T (Q \ K) μ) (hu0 : ∀ x ∈ G, 0 ≤ u x)
    (hcore : ∀ x ∈ Q ∩ K, f x = u x) (htail : ∀ x ∈ Q \ K, f x ≤ T x)
    {ε : ℝ} (hε : (∫ x in Q \ K, T x ∂μ) < ε) :
    (∫ x in Q \ E, f x ∂μ) < (∫ x in G \ E, u x ∂μ) + ε := by
…

theorem OAI.CircleDomainRigidity.FiniteTransfer.integrableOn_coordinateGram_energy line 158

theorem OAI.CircleDomainRigidity.FiniteTransfer.localized_coordinate_energy_lt line 169

Source documentation

The localized estimate for each actual transferred coordinate. The original right-hand side is integrated only over its original domain.

theorem localized_coordinate_energy_lt
    {Ω Q G K : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hG : MeasurableSet G) (hK : IsClosed K) (hQKG : Q ∩ K ⊆ G)
    (f u : ℕ → (ℝ × ℝ) → ℝ) (hf : ∀ i, ContDiffOn ℝ ∞ (f i) Ω)
    {n : ℕ} (hu : ∀ i < n, IntegrableOn
      (gradientEnergy (u i) (fun z => sphericalMetricFactor z • 1)) G)
    (hretain : ∀ᶠ z in 𝓝ˢ K, ∀ i < n, f i z = u i z)
    {g : (ℝ × ℝ) → PlanarMetric} (hg : Continuous g) (hPD : ∀ z, (g z).PosDef)
    (hmetric : ∀ᶠ z in 𝓝ˢ K, g z = sphericalMetricFactor z • 1)
    {ε : ℝ} (henergy : (∫ z in Q \ K, matrixEnergy (coordinateGram f n z) (g z)) < ε)
    {i : ℕ} (hi : i < n) {E : Set (ℝ × ℝ)} (hE : MeasurableSet E) (hEK : E ⊆ K) :
    (∫ z in Q \ E, gradientEnergy (f i) g z) <
…

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