ScalarHalfBallCutoffs.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Nested cutoffs inside the half ball, used after the first local H2 gain.

def OAI.PositiveEinsteinFour.Geometry.scalarHalfBumpGap line 21
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfBumpGap_pos line 23
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfBumpGap_lt line 27
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfBumpGap_succ line 34
def OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedRealBump line 40
Source documentation
A concrete real bump; the gap shrinks geometrically with the index.
```
def scalarHalfNestedRealBump (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1 / 2) (k : ℕ) :
    ContDiffBump (0 : V) where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedRealBump_inner line 51
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedRealBump_outer line 56
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedRealBump_separated line 61
def OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedBumpSchwartz line 70
Source documentation
Complexification turns the actual compact real bump into a Schwartz cutoff.
```
def scalarHalfNestedBumpSchwartz (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1 / 2) (k : ℕ) : S :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedBumpSchwartz_apply line 75
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedBumpSchwartz_tsupport line 79
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedBumpSchwartz_one_nhds line 91
theorem OAI.PositiveEinsteinFour.Geometry.scalarHalfNestedBumpSchwartz_nested line 98

theorem OAI.PositiveEinsteinFour.Geometry.exists_scalar_half_nested_cutoffs line 109

Source documentation

Every compact cutoff inside a smaller closed ball starts a concrete infinite nested sequence supported in the open unit ball.

theorem exists_scalar_half_nested_cutoffs (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1 / 2)
    (φ : S) (hφc : HasCompactSupport (φ : V → ℂ))
    (hφ : tsupport (φ : V → ℂ) ⊆ closedBall 0 r) :
    ∃ ψ : ℕ → S, ψ 0 = φ ∧ (∀ k, ScalarCutoffNested (ψ k) (ψ (k + 1))) ∧
      ∀ k, HasCompactSupport (ψ k : V → ℂ) ∧ tsupport (ψ k : V → ℂ) ⊆ ball 0 (1 / 2) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested