PlanarProjectionGap.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The isolated-well orthogonal gap implies the actual rank-one projection bound on every vector in the closed Sobolev graph. The ground cross term vanishes by the proved variational minimum, without a further spectral input.

def OAI.ContinuumCoulomb.PlanarSobolev.shiftedForm line 19
def OAI.ContinuumCoulomb.PlanarSobolev.shiftedCross line 21
theorem OAI.ContinuumCoulomb.PlanarSobolev.shiftedForm_add_smul line 25
theorem OAI.ContinuumCoulomb.PlanarSobolev.shiftedForm_nonnegative line 36
theorem OAI.ContinuumCoulomb.PlanarSobolev.shiftedForm_normalizedMode line 41
theorem OAI.ContinuumCoulomb.PlanarSobolev.affine_nonnegative_slope_zero line 45
theorem OAI.ContinuumCoulomb.PlanarSobolev.shiftedCross_normalizedMode line 52
theorem OAI.ContinuumCoulomb.PlanarSobolev.shiftedForm_remove_ground line 60
theorem OAI.ContinuumCoulomb.PlanarSobolev.manufacturedPlanarWell_projection_gap line 69
Source documentation
The precise rank-one closed-form bound needed in the multiwell IMS argument, derived from the already cited isolated spectral input.
```
theorem manufacturedPlanarWell_projection_gap (hpublished : ManufacturedPlanarGroundGap) :
    ∃ γ : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ ∀ u : Sobolev,
      ((-1/2 : ℝ) + γ) * ‖u.val.1‖^2 -
        γ * (inner ℝ u.val.1 normalizedMode.val.1)^2 ≤ form u.val := by
…
```
Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PlanarSobolev.Sobolev, OAI.ContinuumCoulomb.PlanarSobolev.form
theorem OAI.ContinuumCoulomb.PlanarSobolev.normalizedMode_ae line 103
theorem OAI.ContinuumCoulomb.PlanarSobolev.graph_normalizedMode_inner line 113
theorem OAI.ContinuumCoulomb.PlanarSobolev.manufacturedPlanarWell_test_projection_gap line 127
Source documentation
The rank-one inequality is attached to the actual normalized planar function and actual test-function integrals used by localization.
```
theorem manufacturedPlanarWell_test_projection_gap (hpublished : ManufacturedPlanarGroundGap) :
    ∃ γ : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ ∀ u : Test,
      ((-1/2 : ℝ) + γ) * (∫ x, u.val x ^ 2) -
        γ * (∫ x, u.val x * normalizedPlanarMode x)^2 ≤
          planarTestForm manufacturedPlanarWell u.val := by
…
```
Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PlanarSobolev.Test, OAI.ContinuumCoulomb.normalizedPlanarMode, OAI.ContinuumCoulomb.planarTestForm, OAI.ContinuumCoulomb.manufacturedPlanarWell
theorem OAI.ContinuumCoulomb.manufacturedPlanarWell_actual_projection_gap line 148
Source documentation
Export the isolated projection inequality with the ambient Euclidean measure used by the actual continuum construction.
```
theorem manufacturedPlanarWell_actual_projection_gap
    (hpublished : PlanarSobolev.ManufacturedPlanarGroundGap) :
    ∃ γ : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ ∀ f : PlanarPosition → ℝ,
      ContDiff ℝ 1 f → HasCompactSupport f →
      ((-1/2 : ℝ) + γ) * (∫ x, f x ^ 2) -
        γ * (∫ x, f x * normalizedPlanarMode x)^2 ≤
          planarTestForm manufacturedPlanarWell f := by
…
```
Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.normalizedPlanarMode, OAI.ContinuumCoulomb.planarTestForm, OAI.ContinuumCoulomb.manufacturedPlanarWell