ScalarPoissonKernelCutoffs.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Concrete nested compact cutoffs inside the unit ball. Their radii tend to one, while each support lies strictly inside the next region of value one.

def OAI.PositiveEinsteinFour.Geometry.scalarBumpGap line 22
theorem OAI.PositiveEinsteinFour.Geometry.scalarBumpGap_pos line 24
theorem OAI.PositiveEinsteinFour.Geometry.scalarBumpGap_lt line 28
theorem OAI.PositiveEinsteinFour.Geometry.scalarBumpGap_succ line 35
def OAI.PositiveEinsteinFour.Geometry.scalarNestedRealBump line 41
Source documentation
A concrete real bump; the gap shrinks geometrically with the index.
```
def scalarNestedRealBump (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (k : ℕ) :
    ContDiffBump (0 : V) where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedRealBump_inner line 52
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedRealBump_outer line 57
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedRealBump_separated line 62
def OAI.PositiveEinsteinFour.Geometry.scalarNestedBumpSchwartz line 71
Source documentation
Complexification turns the actual compact real bump into a Schwartz cutoff.
```
def scalarNestedBumpSchwartz (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1) (k : ℕ) : S :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedBumpSchwartz_apply line 76
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedBumpSchwartz_tsupport line 80
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedBumpSchwartz_one_nhds line 92
theorem OAI.PositiveEinsteinFour.Geometry.scalarNestedBumpSchwartz_nested line 99

theorem OAI.PositiveEinsteinFour.Geometry.exists_scalar_nested_cutoffs line 110

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_nested_cutoffs (r : ℝ) (hr0 : 0 < r) (hr1 : r < 1)
    (φ : 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 := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.ScalarCutoffNested

theorem OAI.PositiveEinsteinFour.Geometry.scalar_ball_local_sobolev line 144

Source documentation

Local H1 and a smooth localized equation imply every local integer Sobolev order; all cutoff-existence obligations are constructed above.

theorem scalar_ball_local_sobolev
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j x, ‖a i j x‖ ≤ δ)
    (ha1 : ∀ i j k x, ‖D k (a i j) x‖ ≤ δ)
    (ha2 : ∀ i j k l x, ‖D k (D l (a i j)) x‖ ≤ δ)
    (hb : ∀ i x, ‖b i x‖ ≤ δ)
    (hb1 : ∀ i k x, ‖D k (b i) x‖ ≤ δ)
    (hsmall : (16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ < 1)
    (u : T)
    (hH1 : ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
      tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev 1 2 (M ψ u))
    (hforce : ∀ n : ℕ, ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_ball_local_sobolev_of_remainder line 171

Source documentation

The geometric remainder P u - u suffices; the solution itself is initially assumed only locally H1.

theorem scalar_ball_local_sobolev_of_remainder
    (a : Fin 4 → Fin 4 → S) (b : Fin 4 → S) (δ : ℝ) (hδ : 0 ≤ δ)
    (ha : ∀ i j x, ‖a i j x‖ ≤ δ)
    (ha1 : ∀ i j k x, ‖D k (a i j) x‖ ≤ δ)
    (ha2 : ∀ i j k l x, ‖D k (D l (a i j)) x‖ ≤ δ)
    (hb : ∀ i x, ‖b i x‖ ≤ δ)
    (hb1 : ∀ i k x, ‖D k (b i) x‖ ≤ δ)
    (hsmall : (16 * (2 * Real.pi) ^ 2 + 36 * (2 * Real.pi) + 20) * δ < 1)
    (u : T)
    (hH1 : ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
      tsupport (ψ : V → ℂ) ⊆ ball 0 1 → MemSobolev 1 2 (M ψ u))
    (hforce : ∀ n : ℕ, ∀ ψ : S, HasCompactSupport (ψ : V → ℂ) →
…