RegularPartition.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MahlerStokes.exists_compact_smooth_partition line 14

Source documentation

An actual smooth partition with compact supports in a given finite bounded open cover, equal to one on a neighborhood of the compact set.

theorem exists_compact_smooth_partition {d : ℕ} {ι : Type} [Fintype ι]
    {K : Set (Fin d → ℝ)} (hK : IsCompact K) (V : ι → Set (Fin d → ℝ))
    (hVo : ∀ i, IsOpen (V i)) (hVb : ∀ i, Bornology.IsBounded (V i))
    (hcover : K ⊆ ⋃ i, V i) :
    ∃ (W : Set (Fin d → ℝ))
      (ρ : SmoothPartitionOfUnity ι 𝓘(ℝ, Fin d → ℝ) (Fin d → ℝ) (closure W)),
      IsOpen W ∧ K ⊆ W ∧ IsCompact (closure W) ∧
      ρ.IsSubordinate V ∧ (∀ i, HasCompactSupport (ρ i)) ∧
      (∀ x ∈ W, ∑ i, ρ i x = 1) := by
…

theorem OAI.MahlerStokes.RegularBoundaryAtlas.exists_partition line 35

Source documentation

The boundary atlas has an actual finite smooth subordinate partition, with compact supports and sum one on a boundary neighborhood.

theorem RegularBoundaryAtlas.exists_partition {d : ℕ} {U K : Set (Fin d → ℝ)}
    {g : (Fin d → ℝ) → ℝ} (a : RegularBoundaryAtlas d U g K) (hK : IsCompact K) :
    ∃ (W : Set (Fin d → ℝ))
      (ρ : SmoothPartitionOfUnity a.Index 𝓘(ℝ, Fin d → ℝ) (Fin d → ℝ) (closure W)),
      IsOpen W ∧ K ⊆ W ∧ IsCompact (closure W) ∧
      (∀ i, tsupport (ρ i) ⊆ (a.patch i).domain) ∧
      (∀ i, HasCompactSupport (ρ i)) ∧ (∀ x ∈ W, ∑ i, ρ i x = 1) :=
…

Mentions: OAI.MahlerStokes.RegularBoundaryAtlas

def OAI.MahlerStokes.sublevelPatchDomain line 47
Source documentation
Adjoin the actual sublevel as the interior patch. This finite cover covers the whole closure, so derivative cancellation can be used throughout D_R.
```
def sublevelPatchDomain {d : ℕ} {U : Set (Fin d → ℝ)} {g : (Fin d → ℝ) → ℝ}
    {R : ℝ} (a : RegularBoundaryAtlas d U g (frontier (regularSublevel U g R))) :
    Option a.Index → Set (Fin d → ℝ)
  | none => regularSublevel U g R
  | some i => (a.patch i).domain
```
Mentions: OAI.MahlerStokes.RegularBoundaryAtlas, OAI.MahlerStokes.regularSublevel
theorem OAI.MahlerStokes.sublevelPatchDomain_covers line 53
theorem OAI.MahlerStokes.exists_sublevel_partition line 66