OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorPromise.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Explicit final weight bounds and promise thresholds for the actual three-stage positive-spin graph.

  1. theorem OAI.ContinuumCoulomb.MediatorIteration.finalGraph_lower line 12
  2. theorem OAI.ContinuumCoulomb.MediatorIteration.finalGraph_upper line 39
  3. theorem OAI.ContinuumCoulomb.MediatorIteration.finalGraph_reciprocal line 75

    Source documentation

    All final positive weights have bounded reciprocals, uniformly over the original signed nonzero coefficients.

    theorem finalGraph_reciprocal {n r W G : ℕ} (F : Bonds n r) (hW : 0 < W) (hG : 0 < G)
    (hJ : ∀ e, |(F.weight e : ℝ)| ≤ W) (hJl : ∀ e, 1 / (W : ℝ) ≤ |(F.weight e : ℝ)|) :
    ∀ e, 1 / ((finalGraph F W G).weight e : ℝ) ≤ 2 := by
…

    Mentions: OAI.ContinuumCoulomb.MediatorIteration.Bonds, OAI.ContinuumCoulomb.MediatorIteration.finalGraph

  4. def OAI.ContinuumCoulomb.MediatorIteration.lowerThreshold line 84
  5. def OAI.ContinuumCoulomb.MediatorIteration.upperThreshold line 87
  6. theorem OAI.ContinuumCoulomb.MediatorIteration.three_stage_yes line 90
  7. theorem OAI.ContinuumCoulomb.MediatorIteration.three_stage_no line 101
  8. theorem OAI.ContinuumCoulomb.MediatorIteration.three_stage_threshold_gap line 113