SmoothCutoffApproximation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Compact cutoffs of actual smooth weak-H1 vectors. This is the cutoff step needed after the published smooth-density theorem.

theorem OAI.ContinuumCoulomb.cutoff_complex_C1 line 13
def OAI.ContinuumCoulomb.smoothCutoffState line 17
theorem OAI.ContinuumCoulomb.smoothCutoffState_gradient line 31

theorem OAI.ContinuumCoulomb.cutoff_product_error_tendsto line 52

Source documentation

Dominated convergence for the two terms in the cutoff product rule.

theorem cutoff_product_error_tendsto {n : ℕ}
    (f g : Configuration n → ℂ) (hf : MemLp f 2) (hg : MemLp g 2)
    (a b : ℕ → Configuration n → ℝ)
    (ha : ∀ k, Continuous (a k)) (hb : ∀ k, Continuous (b k))
    (A B : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hab : ∀ k x, |a k x| ≤ A ∧ |b k x| ≤ B)
    (hat : ∀ x, Tendsto (fun k => a k x) atTop (𝓝 0))
    (hbt : ∀ x, Tendsto (fun k => b k x) atTop (𝓝 0)) :
    Tendsto (fun k => ∫ x, ‖(a k x : ℂ) * f x + (b k x : ℂ) * g x‖^2)
      atTop (𝓝 0) := by
…

Mentions: OAI.ContinuumCoulomb.Configuration

theorem OAI.ContinuumCoulomb.smoothCutoffState_error_tendsto line 95

theorem OAI.ContinuumCoulomb.exists_compact_approximation_of_smooth line 154

Source documentation

Every smooth actual H1 vector is the graph-norm limit of compactly supported C1 vectors, using the existing full-space cutoff construction.

theorem exists_compact_approximation_of_smooth {n : ℕ} (u : Coulomb.H1Vector n)
    (hu : ∀ s, ContDiff ℝ (⊤ : ℕ∞) (u.value s))
    (hd : ∀ s a x, u.gradient s a x = fderiv ℝ (u.value s) x (EuclideanSpace.single a 1))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ v : Coulomb.H1Vector n,
      (∀ s, ContDiff ℝ 1 (v.value s) ∧ HasCompactSupport (v.value s)) ∧
      (∀ s a x, v.gradient s a x =
        fderiv ℝ (v.value s) x (EuclideanSpace.single a 1)) ∧
      h1GraphError u v < ε := by
…

Mentions: OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.h1GraphError