OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ManufacturedFieldBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivatives through order six of the actual three-dimensional manufactured field. Constants do not grow with the number of wells or slab width.

  1. theorem OAI.ContinuumCoulomb.linear_comp_six_bound line 12
  2. def OAI.ContinuumCoulomb.wellPlanarProjection line 26
  3. def OAI.ContinuumCoulomb.wellVerticalProjection line 29
  4. def OAI.ContinuumCoulomb.wellPlanarDerivativeBound line 32
  5. theorem OAI.ContinuumCoulomb.cutoff_derivative_bound_exists line 35
  6. def OAI.ContinuumCoulomb.wellCutoffDerivativeConstant line 41
  7. def OAI.ContinuumCoulomb.wellCutoffDerivativeBound line 43
  8. def OAI.ContinuumCoulomb.manufacturedFieldDerivativeConstant line 46
  9. theorem OAI.ContinuumCoulomb.manufacturedFieldDerivativeConstant_positive line 49
  10. theorem OAI.ContinuumCoulomb.wellPlanar_bound_nonnegative line 56
  11. theorem OAI.ContinuumCoulomb.wellCutoff_bound_nonnegative line 61
  12. theorem OAI.ContinuumCoulomb.manufacturedField_planar_bound line 66
  13. theorem OAI.ContinuumCoulomb.manufacturedField_cutoff_bound line 80
  14. theorem OAI.ContinuumCoulomb.manufacturedWellField_derivative_bound line 100

    Source documentation

    A fixed bound for all six derivatives, uniform over every separated site family, every admissible counterterm and every slab width at least one.

    theorem manufacturedWellField_derivative_bound (freq : ℝ) {scale S : ℝ}
    (hscale : 0 < scale) (hS : 1 ≤ S) {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) (x : Position) :
    ‖iteratedFDeriv ℝ k (manufacturedWellField freq scale S u) x‖ ≤
      manufacturedFieldDerivativeConstant := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.manufacturedWellField, OAI.ContinuumCoulomb.manufacturedFieldDerivativeConstant