OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/H1GraphCore.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The full weak-H1 graph as finitely many actual L2 coordinates. Compact C1 states approximate every coordinate simultaneously, so continuous form inequalities on this graph extend to the full weak-H1 domain.

  1. abbrev OAI.ContinuumCoulomb.H1Index line 14
  2. def OAI.ContinuumCoulomb.h1CoordinateFunction line 16
  3. theorem OAI.ContinuumCoulomb.h1Coordinate_memLp line 21
  4. def OAI.ContinuumCoulomb.h1Coordinates line 27
  5. theorem OAI.ContinuumCoulomb.h1Coordinate_error line 31
  6. theorem OAI.ContinuumCoulomb.h1GraphError_eq_sum line 47
  7. theorem OAI.ContinuumCoulomb.h1Coordinate_error_le line 52
  8. theorem OAI.ContinuumCoulomb.exists_compact_h1_graph_sequence line 60

    Source documentation

    Compact C1 states converge to every actual weak-H1 state in the finite product of value and derivative L2 spaces.

    theorem exists_compact_h1_graph_sequence (hpublished : PublishedSobolevSmoothDensity)
    {n : ℕ} (u : Coulomb.H1Vector n) :
    ∃ v : ℕ → Coulomb.H1Vector n,
      (∀ k s, ContDiff ℝ 1 ((v k).value s) ∧ HasCompactSupport ((v k).value s)) ∧
      (∀ k s a x, (v k).gradient s a x =
        fderiv ℝ ((v k).value s) x (EuclideanSpace.single a 1)) ∧
      Tendsto (fun k => h1Coordinates (v k)) atTop (𝓝 (h1Coordinates u)) := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.h1Coordinates

  9. theorem OAI.ContinuumCoulomb.h1_continuous_nonnegative_of_compact line 87

    Source documentation

    Transfer a continuous inequality from compact classical states to the full declared weak-H1 graph.

    theorem h1_continuous_nonnegative_of_compact
    (hpublished : PublishedSobolevSmoothDensity) {n : ℕ}
    (F : (H1Index n → Lp ℂ 2 (volume : Measure (Configuration n))) → ℝ)
    (hF : Continuous F)
    (hcompact : ∀ 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)) → 0 ≤ F (h1Coordinates v))
    (u : Coulomb.H1Vector n) : 0 ≤ F (h1Coordinates u) := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedSobolevSmoothDensity, OAI.ContinuumCoulomb.H1Index, OAI.ContinuumCoulomb.Configuration, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.h1Coordinates