OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourceMatrix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Identification of the encoded source's original swap-form variational energy with the complete finite matrix used by all mediator stages.

  1. def OAI.ContinuumCoulomb.SquareLatticeHeisenberg.bonds line 13
  2. theorem OAI.ContinuumCoulomb.sourceSpinMass_norm_sq line 19
  3. theorem OAI.ContinuumCoulomb.sourceGraphMatrix_action line 24
  4. theorem OAI.ContinuumCoulomb.sourceGraphMatrix_form line 34
  5. theorem OAI.ContinuumCoulomb.sourceMatrixBottom_eq_realSource line 50

    Source documentation

    The mediator input is the actual source energy in the published promise.

    theorem sourceMatrixBottom_eq_realSource (d : SquareLatticeHeisenberg) :
    sourceMatrixBottom d.vertices d.bonds.matrix = realSourceGroundEnergy d := by
…

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

  6. theorem OAI.ContinuumCoulomb.source_three_stage_bottom line 66