OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarGroundTransform.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The planar manufactured well's ground-state transform. Integration by parts establishes positivity on actual compact C¹ test functions. Existence, decay and the excitation gap of the specific resolvent-generated mode remain separate analytic steps.

  1. abbrev OAI.ContinuumCoulomb.PlanarPosition line 15
  2. def OAI.ContinuumCoulomb.planarPartial line 17
  3. def OAI.ContinuumCoulomb.planarAxis line 20
  4. def OAI.ContinuumCoulomb.planarLaplacian line 22
  5. theorem OAI.ContinuumCoulomb.planarPartial_C1 line 25
  6. theorem OAI.ContinuumCoulomb.planarPartial_continuous line 29
  7. theorem OAI.ContinuumCoulomb.planarPartial_mul line 34
  8. theorem OAI.ContinuumCoulomb.planarPartial_mul_square line 42
  9. theorem OAI.ContinuumCoulomb.planar_transform_integrable line 54
  10. theorem OAI.ContinuumCoulomb.planar_transform_ibp line 80
  11. theorem OAI.ContinuumCoulomb.planar_ground_transform_direction line 92
  12. theorem OAI.ContinuumCoulomb.planar_ground_transform_nonnegative line 118

    Source documentation

    Nonnegativity of the shifted manufactured-well form on compact C¹ tests follows from the actual directional integration-by-parts identities.

    theorem planar_ground_transform_nonnegative (phi v : PlanarPosition → ℝ)
    (hphi : ContDiff ℝ 2 phi) (hv : ContDiff ℝ 1 v) (hc : HasCompactSupport v) :
    0 ≤ ∑ a : Fin 2, ∫ x,
      planarPartial (fun y => phi y * v y) (planarAxis a) x ^ 2 +
        phi x * planarPartial (planarPartial phi (planarAxis a)) (planarAxis a) x * v x ^ 2 := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarPartial, OAI.ContinuumCoulomb.planarAxis

  13. def OAI.ContinuumCoulomb.planarTestForm line 128
  14. theorem OAI.ContinuumCoulomb.planar_partial_square_integrable line 132
  15. theorem OAI.ContinuumCoulomb.planar_transform_energy_split line 140
  16. theorem OAI.ContinuumCoulomb.planar_positive_mode_form_lower line 167

    Source documentation

    A positive classical mode at energy -1/2 gives the lower bound on every compact C¹ test, without assuming the well's spectral conclusion.

    theorem planar_positive_mode_form_lower (phi W u : PlanarPosition → ℝ)
    (hphi : ContDiff ℝ 2 phi) (hpos : ∀ x, 0 < phi x) (hW : Continuous W)
    (heigen : ∀ x, planarLaplacian phi x = (2 * W x + 1) * phi x)
    (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) :
    -(1 / 2 : ℝ) * (∫ x, u x ^ 2) ≤ planarTestForm W u := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarLaplacian, OAI.ContinuumCoulomb.planarTestForm