OAI/Geometry/RCD/Sobolev/NullCompactCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous cutoffs of null compact sets with vanishing L² norm

  1. theorem OAI.RegularPointCoordinates.compactTestToL2_norm_sq_le line 17
  2. theorem OAI.RegularPointCoordinates.exists_null_compact_cutoffs line 40

    Source documentation

    Outer regularity supplies continuous unit cutoffs of a null compact set whose actual L² classes converge to zero.

    theorem exists_null_compact_cutoffs {S : Set X} (hS : IsCompact S) (hnull : μ S = 0) :
    ∃ F : ℕ → C_c(X, ℝ),
      (∀ i x, 0 ≤ F i x ∧ F i x ≤ 1) ∧
      (∀ i, EqOn (F i) 1 S) ∧
      Tendsto (fun i => compactTestToL2 μ (F i)) atTop (𝓝 0) := by
…

    Mentions: OAI.RegularPointCoordinates.compactTestToL2