OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedWellField.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The actual compact three-dimensional well field in the unit-charge construction. Its coefficients are Coulomb counterterms. The cutoff only weakens the attractive uncorrected wells.

  1. def OAI.ContinuumCoulomb.slabWellCutoff line 16
  2. theorem OAI.ContinuumCoulomb.slabWellCutoff_bounds line 18
  3. theorem OAI.ContinuumCoulomb.slabWellCutoff_smooth line 22
  4. theorem OAI.ContinuumCoulomb.slabWellCutoff_inner line 25
  5. theorem OAI.ContinuumCoulomb.slabWellCutoff_outer line 34
  6. def OAI.ContinuumCoulomb.countertermWellSum line 43
  7. def OAI.ContinuumCoulomb.manufacturedWellField line 47
  8. theorem OAI.ContinuumCoulomb.countertermWellSum_C7 line 52
  9. theorem OAI.ContinuumCoulomb.manufacturedWellField_C7 line 58
  10. theorem OAI.ContinuumCoulomb.countertermWellSum_nonpositive line 64
  11. theorem OAI.ContinuumCoulomb.manufacturedWellField_nonpositive line 73
  12. theorem OAI.ContinuumCoulomb.manufacturedWellField_inner line 79
  13. theorem OAI.ContinuumCoulomb.manufacturedWellField_outer line 86
  14. theorem OAI.ContinuumCoulomb.countertermWellSum_zero_far line 92
  15. theorem OAI.ContinuumCoulomb.manufacturedWellField_support line 99
  16. theorem OAI.ContinuumCoulomb.manufacturedWellField_compact line 125
  17. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_fst_zero line 135
  18. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_fst_one line 138
  19. theorem OAI.ContinuumCoulomb.positionSplitCoordinates_snd line 141
  20. theorem OAI.ContinuumCoulomb.manufacturedWellField_support_slab line 144
  21. theorem OAI.ContinuumCoulomb.well_zero_away_from_near_site line 171
  22. theorem OAI.ContinuumCoulomb.countertermWellSum_lower line 182

    Source documentation

    Disjoint planar supports prevent the counterterm perturbation from growing with the number of sites.

    theorem countertermWellSum_lower (freq scale : ℝ) {m : ℕ}
    (u : Fin m → PlanarPosition) (hsep : ∀ i j, i ≠ j → 2 ≤ ‖u i-u j‖)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hcoeff : ∀ i, 0 ≤ localizedCounterterm freq u i / scale ∧
      localizedCounterterm freq u i / scale ≤ δ) (r : PlanarPosition) :
    planarWellSum u r - δ*PlanarSobolev.wellBound ≤ countertermWellSum freq scale u r := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.planarWellSum, OAI.ContinuumCoulomb.PlanarSobolev.wellBound, OAI.ContinuumCoulomb.countertermWellSum

  23. theorem OAI.ContinuumCoulomb.manufacturedWellField_lower line 212

    Source documentation

    Global lower comparison to the separable uncapped multiwell field.

    theorem manufacturedWellField_lower (freq : ℝ) {scale : ℝ} (hscale : 0 ≤ scale)
    (S : ℝ) {m : ℕ} (u : Fin m → PlanarPosition)
    (hsep : ∀ i j, i ≠ j → 2 ≤ ‖u i-u j‖) {δ : ℝ} (hδ : 0 ≤ δ)
    (hcoeff : ∀ i, 0 ≤ localizedCounterterm freq u i / scale ∧
      localizedCounterterm freq u i / scale ≤ δ) (x : Position) :
    planarWellSum u (positionSplitCoordinates x).1 - δ*PlanarSobolev.wellBound ≤
      manufacturedWellField freq scale S u x := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.planarWellSum, OAI.ContinuumCoulomb.positionSplitCoordinates, OAI.ContinuumCoulomb.PlanarSobolev.wellBound, OAI.ContinuumCoulomb.manufacturedWellField