OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CompactSobolevCore.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported C1 approximation on the full declared weak-H1 configuration domain. Only the explicitly cited smooth-density input is conditional; the compactification step is proved here.

  1. theorem OAI.ContinuumCoulomb.integral_square_error_triangle line 14
  2. theorem OAI.ContinuumCoulomb.h1GraphError_triangle line 36
  3. theorem OAI.ContinuumCoulomb.exists_compact_h1_approximation line 52

    Source documentation

    The smooth-density theorem plus the proved cutoff step gives a compact core for the actual full weak-H1 vectors, with no symmetry restriction.

    theorem exists_compact_h1_approximation (hpublished : PublishedSobolevSmoothDensity)
    {n : ℕ} (u : Coulomb.H1Vector n) {ε : ℝ} (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.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.h1GraphError