FiniteTransferEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Common-width selection with actual transferred energy bounds

After the geometric disk construction, one sufficiently late width gives smooth filled coordinates, a metric retaining the spherical background, and both the total and localized energy estimates. The cost is measured only on the original domain. Periodic and masked coordinates are treated separately from this real-coordinate analytic assembly.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_filled_spherical_transfer_at_good_width line 26

Source documentation

Analytic assembly for a finite family of real coordinates. The geometric filling premise is eventual in width, so it is met at the same width that gives the cost estimate.

theorem exists_filled_spherical_transfer_at_good_width
    {I : Type*} [Fintype I] {n : ℕ}
    (D : I → Set (ℝ × ℝ)) (hD : ∀ i, IsOpen (D i))
    {Ω Q G K : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hG : MeasurableSet G) (hK : IsClosed K) (hKG : K ⊆ G)
    (hcover : Q ⊆ G ∪ ⋃ i, D i) (hKD : ∀ x ∈ K, ∀ i, x ∉ D i)
    (v : ℝ → Fin n → (ℝ × ℝ) → ℝ) (u : Fin n → (ℝ × ℝ) → ℝ)
    (hu : ∀ i, MemLp (planarGradient (u i)) 2 (volume.restrict G))
    (hretain : ∀ δ, ∀ᶠ x in 𝓝ˢ K, ∀ i, v δ i x = u i x)
    {h : ℝ} (hh : 0 < h)
    (hfill : ∀ᶠ δ : ℝ in 𝓝[>] 0, ∃ F : Fin n → (ℝ × ℝ) → ℝ,
      IsFilledCoordinateFamily D Ω (v δ) F)
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient, OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily