OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarIMSBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative IMS lower bounds, attached to the actual separated-site partition. The error constant depends on one fixed bump and D, not on the number of sites.

  1. theorem OAI.ContinuumCoulomb.planar_localization_cost_integrable line 14
  2. theorem OAI.ContinuumCoulomb.planar_IMS_cost_bound line 26
  3. theorem OAI.ContinuumCoulomb.planar_IMS_lower line 45
  4. theorem OAI.ContinuumCoulomb.planarSitePartition_IMS_lower line 59

    Source documentation

    An actual multiwell localization estimate with fixed bump constant and quadratic inverse-separation error.

    theorem planarSitePartition_IMS_lower {ι : Type*} [Fintype ι] {D : ℝ} (hD : 0 < D)
    (u : ι → PlanarPosition) (hsep : ∀ i j, i ≠ j → D ≤ ‖u i-u j‖)
    (W f : PlanarPosition → ℝ) (hW : Continuous W)
    (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
    (∑ i, planarTestForm W (fun x => planarSitePartition D u i x * f x)) -
      planarSiteDerivativeBound D ^ 2 * (∫ x, f x ^ 2) ≤ planarTestForm W f := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarTestForm, OAI.ContinuumCoulomb.planarSitePartition, OAI.ContinuumCoulomb.planarSiteDerivativeBound