OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarFieldBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual planar counterterm field has uniform derivative bounds, independent of the number of sites. Separated unit supports leave at most one nonzero summand at every point.

  1. theorem OAI.ContinuumCoulomb.planarWell_derivatives_bounded line 14
  2. def OAI.ContinuumCoulomb.planarWellDerivativeConstant line 32
  3. theorem OAI.ContinuumCoulomb.planarWellDerivativeConstant_positive line 34
  4. theorem OAI.ContinuumCoulomb.planarWellDerivativeConstant_bound line 37
  5. theorem OAI.ContinuumCoulomb.well_derivative_near line 41
  6. theorem OAI.ContinuumCoulomb.countertermWellSum_derivative line 47
  7. theorem OAI.ContinuumCoulomb.countertermWellSum_derivative_bound line 69

    Source documentation

    Uniformity in the number of separated sites is essential for the polynomial-time transport/cubature constants.

    theorem countertermWellSum_derivative_bound (freq : ℝ) {scale : ℝ} (hscale : 0 < scale)
    {m : ℕ} (u : Fin m → PlanarPosition)
    (hsep : ∀ i j, i ≠ j → 3 ≤ ‖u i-u j‖)
    (hcounter : ∀ i, localizedCounterterm freq u i ≤ scale)
    {k : ℕ} (hk : k ≤ 6) (r : PlanarPosition) :
    ‖iteratedFDeriv ℝ k (countertermWellSum freq scale u) r‖ ≤
      2*planarWellDerivativeConstant := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.countertermWellSum, OAI.ContinuumCoulomb.planarWellDerivativeConstant