RegularCore.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A regular retained core containing infinity

Only the already stated planar Sard input is used for the regular value. The core may contain an arbitrary closed subset of the domain. Its complement has compact closure in the finite chart, so the core retains an entire neighborhood of infinity.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_real_regular_value_in_interval line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_real_cutoff line 38

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_regular_core_small_tail line 57

Source documentation

Sard selects a regular level separating a prescribed closed part of the physical domain from all its complementary components. Finite energy makes the remaining tail small.

theorem exists_regular_core_small_tail (hsard : SmoothPlanarSard)
    {G K₀ : Set (ℝ × ℝ)} (hG : IsOpen G) (hGc : IsCompact Gᶜ)
    (hK₀ : IsClosed K₀) (hK₀G : K₀ ⊆ G)
    {f : (ℝ × ℝ) → ℝ} (hf : IntegrableOn f G) (hf0 : ∀ z, 0 ≤ f z)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (ψ : (ℝ × ℝ) → ℝ) (t : ℝ) (K : Set (ℝ × ℝ)),
      ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧ t ∈ Ioo 0 1 ∧
      (∀ z, ψ z = t → fderiv ℝ ψ z ≠ 0) ∧ K = {z | ψ z ≤ t} ∧
      IsClosed K ∧ K₀ ⊆ interior K ∧ K ⊆ G ∧ IsCompact (closure Kᶜ) ∧
      (∫ z in G \ K, f z) < ε := by
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_cutoff_near_complement line 118

Source documentation

For a domain containing infinity the cutoff is compactly supported in the finite chart, vanishes near the entire retained core and equals one near every missing component.

theorem exists_cutoff_near_complement
    {G K : Set (ℝ × ℝ)} (hGc : IsCompact Gᶜ) (hK : IsClosed K) (hKG : K ⊆ G) :
    ∃ χ : (ℝ × ℝ) → ℝ, ContDiff ℝ ∞ χ ∧ HasCompactSupport χ ∧
      (∀ z, χ z ∈ Icc 0 1) ∧ (∀ᶠ z in 𝓝ˢ K, χ z = 0) ∧
      (∀ᶠ z in 𝓝ˢ Gᶜ, χ z = 1) ∧ MemLp (planarGradient χ) 2 volume := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient