CofiniteTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Energy transfer on a completed region containing infinity

The completed region is unbounded in a finite chart. Its tail outside the retained core lies in one compact piece. Local agreement on the core and the original finite energy give integrability on the entire completed region, and hence the full localized estimate.

theorem OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy_eq_spherical_on_core line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.integrableOn_gradientEnergy_with_cofinite_core line 31
theorem OAI.CircleDomainRigidity.FiniteTransfer.localized_coordinate_energy_lt_with_cofinite_core line 50

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_cofinite_transfer_at_good_width line 81

Source documentation

The common-width analytic transfer applies to the entire completed region, including its unbounded chart part, whenever the core retains infinity.

theorem exists_cofinite_transfer_at_good_width
    {I : Type*} [Fintype I] {n : ℕ}
    (D : I → Set (ℝ × ℝ)) (hD : ∀ i, IsOpen (D i))
    {Ω Q G K : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsClosed Q) (hQΩ : Q ⊆ Ω)
    (hG : MeasurableSet G) (hK : IsClosed K) (hKc : IsCompact (closure 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