PlanarMultiwellProjection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A global multiwell lower bound on every test function, with actual uncut orbital coefficients. This form of the estimate is stable under H1 approximation and tensor products; no exact orthogonality of approximants is needed.

theorem OAI.ContinuumCoulomb.cutoff_add_sq_le line 15
theorem OAI.ContinuumCoulomb.planarSiteCutoff_pair_error line 25
theorem OAI.ContinuumCoulomb.planarSiteCutoff_pair_bound line 49

theorem OAI.ContinuumCoulomb.planarWellSum_test_projection_bound line 63

Source documentation

Global lower bound with explicitly controlled finite orbital form and cutoff error. The only spectral input is the published isolated-well gap.

theorem planarWellSum_test_projection_bound
    (hpublished : PlanarSobolev.ManufacturedPlanarGroundGap) :
    ∃ γ : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ ∀ (m : ℕ) (D η : ℝ), 8 ≤ D → 0 < η →
      ∀ u : Fin m → PlanarPosition, (∀ i j, i ≠ j → D ≤ ‖u i-u j‖) →
      ∀ f : PlanarPosition → ℝ, ContDiff ℝ 1 f → HasCompactSupport f →
      ((-1/2:ℝ)+γ-planarSiteDerivativeBound D^2-
        γ*(1+η⁻¹)*m*planarSiteTailConstant*Real.exp (-(19/20:ℝ)*(D/8)))*(∫ x, f x^2) -
        γ*(1+η)*(∑ i, (∫ x, f x*normalizedPlanarMode (x-u i))^2) ≤
          planarTestForm (planarWellSum u) f := by
…

Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarSiteDerivativeBound, OAI.ContinuumCoulomb.planarSiteTailConstant, OAI.ContinuumCoulomb.normalizedPlanarMode, OAI.ContinuumCoulomb.planarTestForm, OAI.ContinuumCoulomb.planarWellSum