ScalarPoissonKernelLocalTests.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Compact tests determine every inner localization of a distribution. A source smooth only on the test domain becomes a Schwartz source after localization, and therefore has all Sobolev orders.

theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_cutoff_compact line 21
theorem OAI.PositiveEinsteinFour.Geometry.scalarSchwartz_cutoff_support line 27

theorem OAI.PositiveEinsteinFour.Geometry.scalar_localize_eq_of_compact_tests line 35

Source documentation

Equality on compact tests in U gives equality after any compact Schwartz cutoff supported in U.

theorem scalar_localize_eq_of_compact_tests (U : Set V) (u v : T)
    (htest : ∀ φ : S, HasCompactSupport (φ : V → ℂ) →
      tsupport (φ : V → ℂ) ⊆ U → u φ = v φ)
    (ψ : S) (hc : HasCompactSupport (ψ : V → ℂ))
    (hs : tsupport (ψ : V → ℂ) ⊆ U) :
    M ψ u = M ψ v := by
…

theorem OAI.PositiveEinsteinFour.Geometry.scalar_localize_zero_of_compact_tests line 45
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalSource_smooth line 55
def OAI.PositiveEinsteinFour.Geometry.scalarLocalSourceSchwartz line 69
Source documentation
A smooth source restricted by a compact Schwartz cutoff is Schwartz, even if it has no regularity or growth control outside the cutoff.
```
def scalarLocalSourceSchwartz (ψ : S) (f : V → ℂ)
    (hc : HasCompactSupport (ψ : V → ℂ))
    (hf : ∀ x ∈ tsupport (ψ : V → ℂ), ContDiffAt ℝ (⊤ : ℕ∞) f x) : S :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.scalarLocalSourceSchwartz_apply line 74

theorem OAI.PositiveEinsteinFour.Geometry.scalar_localize_eq_smooth_source line 81

Source documentation

The actual compact-test equation identifies the localized source with a constructed Schwartz function.

theorem scalar_localize_eq_smooth_source (U : Set V) (u : T) (f : V → ℂ)
    (hf : ∀ x ∈ U, ContDiffAt ℝ (⊤ : ℕ∞) f x)
    (htest : ∀ φ : S, HasCompactSupport (φ : V → ℂ) →
      tsupport (φ : V → ℂ) ⊆ U → u φ = ∫ x, φ x * f x)
    (ψ : S) (hc : HasCompactSupport (ψ : V → ℂ))
    (hs : tsupport (ψ : V → ℂ) ⊆ U) :
    M ψ u = (scalarLocalSourceSchwartz ψ f hc (fun x hx => hf x (hs hx)) : T) := by
…

Mentions: OAI.PositiveEinsteinFour.Geometry.scalarLocalSourceSchwartz

theorem OAI.PositiveEinsteinFour.Geometry.scalar_localize_smooth_source_memSobolev line 100

Source documentation

A compact-test equation with a locally smooth source supplies all orders of the inner localized forcing used by the elliptic bootstrap.

theorem scalar_localize_smooth_source_memSobolev (U : Set V) (u : T) (f : V → ℂ)
    (hf : ∀ x ∈ U, ContDiffAt ℝ (⊤ : ℕ∞) f x)
    (htest : ∀ φ : S, HasCompactSupport (φ : V → ℂ) →
      tsupport (φ : V → ℂ) ⊆ U → u φ = ∫ x, φ x * f x)
    (ψ : S) (hc : HasCompactSupport (ψ : V → ℂ))
    (hs : tsupport (ψ : V → ℂ) ⊆ U) (s : ℝ) :
    MemSobolev s 2 (M ψ u) := by
…