PlanarMultiwellGap.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The actual planar multiwell form has a fixed excitation gap away from the span of the translated manufactured modes, up to explicit inverse-square localization and exponential tail errors. No multiwell spectral input is used.

theorem OAI.ContinuumCoulomb.planar_partition_mass line 16
theorem OAI.ContinuumCoulomb.planar_free_form_nonnegative line 37
theorem OAI.ContinuumCoulomb.planarWellSum_projection_lower line 44
theorem OAI.ContinuumCoulomb.planarSiteCutoff_pair_of_orthogonal line 77

theorem OAI.ContinuumCoulomb.planarWellSum_test_complement_bound line 106

Source documentation

Quantitative actual test-domain multiwell complement bound. The only conditional input is the cited isolated planar gap; every localization and cutoff loss in this formula has been proved for the manufactured functions.

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

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