OAI/Analysis/CircleDomains/Topology/CoreCutoff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual cutoff used in grid modification

A compact retained core in the open physical domain admits a globally smooth cutoff, zero near the core and one off a larger compact subset of the domain. Its gradient is square-integrable without an extra premise.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_planarGradient line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.hasCompactSupport_planarGradient line 26
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.planarGradient_const_sub line 34
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_core_cutoff line 40

    Source documentation

    The cutoff and its L² differential are constructed, rather than supplied to the subsequent random-grid argument.

    theorem exists_core_cutoff
    {G K : Set (ℝ × ℝ)} (hG : IsOpen G) (hK : IsCompact K) (hKG : K ⊆ G) :
    ∃ (χ : (ℝ × ℝ) → ℝ) (L : Set (ℝ × ℝ)),
      ContDiff ℝ ∞ χ ∧ IsCompact L ∧ L ⊆ G ∧
      (∀ z, χ z ∈ Icc 0 1) ∧ (∀ᶠ z in 𝓝ˢ K, χ z = 0) ∧
      (∀ z ∉ L, χ z = 1) ∧ MemLp (planarGradient χ) 2 volume := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.planarGradient