SmallEnergyCore.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Choosing the retained core from finite energy

Compact exhaustion of the actual open domain makes the original wedge integral arbitrarily small. An intervening open neighborhood puts every prescribed compact subset strictly inside the selected compact core.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compact_core_small_tail line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_coordinateWedges_of_memLp line 59

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compact_core_small_wedges line 70

Source documentation

The original L² coordinates supply the small-wedge premise needed by grid selection, after retaining any prescribed compact subset.

theorem exists_compact_core_small_wedges
    {G K₀ : Set (ℝ × ℝ)} (hG : IsOpen G) (hK₀ : IsCompact K₀) (hK₀G : K₀ ⊆ G)
    {n : ℕ} (u : Fin n → (ℝ × ℝ) → ℝ)
    (hu : ∀ i, MemLp (planarGradient (u i)) 2 (volume.restrict G))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ K : Set (ℝ × ℝ), IsCompact K ∧ K₀ ⊆ interior K ∧ K ⊆ G ∧
      (∫ z in G \ K, coordinateWedges (natCoordinateFamily u) n z) < ε := by
…

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