OAI/Geometry/RCD/Coordinates/RegularCompactCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Compact cutoffs with an L² Laplacian on arbitrary open sets

  1. structure OAI.RegularPointCoordinates.RegularCompactCutoff line 18

    Source documentation

    Qualitative cutoff data, without a fixed ratio between the two radii.

    structure RegularCompactCutoff where
…
  2. def OAI.RegularPointCoordinates.RegularCompactCutoff.zero line 33
  3. lemma OAI.RegularPointCoordinates.RegularCompactCutoff.abs_le line 45
  4. def OAI.RegularPointCoordinates.RegularCompactCutoff.union line 50

    Source documentation

    Combining two plateaux preserves their union and the L² Laplacian.

    def union (χ η : RegularCompactCutoff μ hQ) : RegularCompactCutoff μ hQ := by
…

    Mentions: OAI.RegularPointCoordinates.RegularCompactCutoff

  5. lemma OAI.RegularPointCoordinates.RegularCompactCutoff.union_weight line 92
  6. lemma OAI.RegularPointCoordinates.RegularCompactCutoff.union_support line 95
  7. lemma OAI.RegularPointCoordinates.RegularCompactCutoff.union_one_left line 101
  8. lemma OAI.RegularPointCoordinates.RegularCompactCutoff.union_one_right line 107