SourceSpectrum.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Source spectral bottom and rational normalization

The bottom ranges over every normalized many-spin vector. Uniform coefficient error controls that variational bottom and the YES/NO thresholds of the square-lattice Heisenberg problem.

def OAI.ContinuumCoulomb.allUpSourceBasis line 20
def OAI.ContinuumCoulomb.allUpSourceVector line 22
theorem OAI.ContinuumCoulomb.allUpSourceVector_mass line 25
theorem OAI.ContinuumCoulomb.sourceHamiltonianForm_abs_le line 30
Source documentation
Uniform form bound for the complete signed source Hamiltonian.
```
theorem sourceHamiltonianForm_abs_le (d : SquareLatticeHeisenberg)
    (u : SourceSpinVector d.vertices) :
    |sourceHamiltonianForm d u| ≤
      (3 * ∑ e, |(d.coefficient e : ℝ)|) * sourceSpinMass u := by
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.sourceHamiltonianForm, OAI.ContinuumCoulomb.sourceSpinMass
theorem OAI.ContinuumCoulomb.sourceGroundEnergy_le_trial line 49
theorem OAI.ContinuumCoulomb.sourceGroundEnergy_lower_of_forall line 54
theorem OAI.ContinuumCoulomb.sourceGroundEnergy_lower_bound line 63
theorem OAI.ContinuumCoulomb.sourceGroundEnergy_ne_bot line 70
theorem OAI.ContinuumCoulomb.sourceGroundEnergy_ne_top line 74
def OAI.ContinuumCoulomb.realSourceGroundEnergy line 81
Source documentation
The finite source bottom, now known to be a real number.
```
def realSourceGroundEnergy (d : SquareLatticeHeisenberg) : ℝ :=
…
```
Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg
theorem OAI.ContinuumCoulomb.realSourceGroundEnergy_coe line 84
theorem OAI.ContinuumCoulomb.realSourceGroundEnergy_le_trial line 88
theorem OAI.ContinuumCoulomb.realSourceGroundEnergy_lower_of_forall line 95
def OAI.ContinuumCoulomb.SquareLatticeHeisenberg.withCoefficients line 104

theorem OAI.ContinuumCoulomb.realSourceGroundEnergy_rounding line 109

Source documentation

Uniform perturbation of every state controls both variational bottoms.

theorem realSourceGroundEnergy_rounding (d : SquareLatticeHeisenberg)
    (rounded : Fin d.edges → ℚ) :
    |realSourceGroundEnergy (d.withCoefficients rounded) - realSourceGroundEnergy d| ≤
      3 * ∑ e, |(d.coefficient e : ℝ) - (rounded e : ℝ)| := by
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.realSourceGroundEnergy

theorem OAI.ContinuumCoulomb.sourceNormalization_energy_error line 137

Source documentation

The smallest useful energy consequence of coefficient rounding and scalar-term removal for the source normalization.

theorem sourceNormalization_energy_error (d : SquareLatticeHeisenberg)
    (rounded : Fin d.edges → ℚ) (c ε : ℝ)
    (hcoeff : (∑ e, |(d.coefficient e : ℝ) - (rounded e : ℝ)|) ≤ ε) :
    |realSourceGroundEnergy (d.withCoefficients rounded) -
      ((realSourceGroundEnergy d + c) - c)| ≤ 3 * ε := by
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.realSourceGroundEnergy

theorem OAI.ContinuumCoulomb.sourceNormalization_yes line 147

Source documentation

Actual spectral-bottom rounding preserves the source YES implication.

theorem sourceNormalization_yes (d : SquareLatticeHeisenberg)
    (rounded : Fin d.edges → ℚ) {c a aRound cRound ε : ℝ}
    (hcoeff : (∑ e, |(d.coefficient e : ℝ) - (rounded e : ℝ)|) ≤ ε)
    (ha : |aRound - a| ≤ ε) (hc : |cRound - c| ≤ ε)
    (hyes : realSourceGroundEnergy d + c ≤ a) :
    realSourceGroundEnergy (d.withCoefficients rounded) ≤
      normalizedSourceLower aRound cRound ε :=
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.realSourceGroundEnergy, OAI.ContinuumCoulomb.normalizedSourceLower

theorem OAI.ContinuumCoulomb.sourceNormalization_no line 157

Source documentation

Actual spectral-bottom rounding preserves the source NO implication.

theorem sourceNormalization_no (d : SquareLatticeHeisenberg)
    (rounded : Fin d.edges → ℚ) {c b bRound cRound ε : ℝ}
    (hcoeff : (∑ e, |(d.coefficient e : ℝ) - (rounded e : ℝ)|) ≤ ε)
    (hb : |bRound - b| ≤ ε) (hc : |cRound - c| ≤ ε)
    (hno : b ≤ realSourceGroundEnergy d + c) :
    normalizedSourceUpper bRound cRound ε ≤
      realSourceGroundEnergy (d.withCoefficients rounded) :=
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.realSourceGroundEnergy, OAI.ContinuumCoulomb.normalizedSourceUpper

theorem OAI.ContinuumCoulomb.sourceNormalization line 168

Source documentation

Source normalization with the papers' error allocation, retaining the two promise implications and at least 22δ/25 threshold separation.

theorem sourceNormalization (d : SquareLatticeHeisenberg)
    (rounded : Fin d.edges → ℚ) {c a b aRound bRound cRound δ : ℝ}
    (hgap : δ ≤ b - a)
    (hcoeff : (∑ e, |(d.coefficient e : ℝ) - (rounded e : ℝ)|) ≤ δ / 100)
    (ha : |aRound - a| ≤ δ / 100)
    (hb : |bRound - b| ≤ δ / 100)
    (hc : |cRound - c| ≤ δ / 100) :
    (realSourceGroundEnergy d + c ≤ a →
      realSourceGroundEnergy (d.withCoefficients rounded) ≤
        normalizedSourceLower aRound cRound (δ / 100)) ∧
    (b ≤ realSourceGroundEnergy d + c →
      normalizedSourceUpper bRound cRound (δ / 100) ≤
…

Mentions: OAI.ContinuumCoulomb.SquareLatticeHeisenberg, OAI.ContinuumCoulomb.realSourceGroundEnergy, OAI.ContinuumCoulomb.normalizedSourceLower, OAI.ContinuumCoulomb.normalizedSourceUpper