OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorIteration.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

The three actual mediator stages. Only the original central bonds survive the last subdivision; each original spoke becomes a nine-link path, giving eighteen new spins and nineteen positive bonds per edge.

  1. structure OAI.ContinuumCoulomb.MediatorIteration.Bonds line 14
  2. def OAI.ContinuumCoulomb.MediatorIteration.Bonds.NoLoops line 19
  3. def OAI.ContinuumCoulomb.MediatorIteration.Bonds.matrix line 21
  4. def OAI.ContinuumCoulomb.MediatorIteration.empty line 25
  5. def OAI.ContinuumCoulomb.MediatorIteration.lift line 30
  6. def OAI.ContinuumCoulomb.MediatorIteration.central line 35
  7. def OAI.ContinuumCoulomb.MediatorIteration.spokes line 40
  8. def OAI.ContinuumCoulomb.MediatorIteration.join line 48
  9. theorem OAI.ContinuumCoulomb.MediatorIteration.empty_noLoops line 53
  10. theorem OAI.ContinuumCoulomb.MediatorIteration.lift_noLoops line 55
  11. theorem OAI.ContinuumCoulomb.MediatorIteration.central_noLoops line 60
  12. theorem OAI.ContinuumCoulomb.MediatorIteration.spokes_noLoops line 66
  13. theorem OAI.ContinuumCoulomb.MediatorIteration.join_noLoops line 71
  14. theorem OAI.ContinuumCoulomb.MediatorIteration.join_matrix line 79
  15. theorem OAI.ContinuumCoulomb.MediatorIteration.empty_matrix line 85
  16. theorem OAI.ContinuumCoulomb.MediatorIteration.stage_matrix_split line 88
  17. def OAI.ContinuumCoulomb.MediatorIteration.secondBound line 102
  18. def OAI.ContinuumCoulomb.MediatorIteration.thirdBound line 103
  19. def OAI.ContinuumCoulomb.MediatorIteration.member line 105
  20. theorem OAI.ContinuumCoulomb.MediatorIteration.member_eq line 107
  21. def OAI.ContinuumCoulomb.MediatorIteration.deltaOne line 110
  22. def OAI.ContinuumCoulomb.MediatorIteration.deltaTwo line 111
  23. def OAI.ContinuumCoulomb.MediatorIteration.deltaThree line 112
  24. def OAI.ContinuumCoulomb.MediatorIteration.firstCentral line 115
  25. def OAI.ContinuumCoulomb.MediatorIteration.firstSpokes line 118
  26. def OAI.ContinuumCoulomb.MediatorIteration.secondCentral line 122
  27. def OAI.ContinuumCoulomb.MediatorIteration.secondSpokes line 125
  28. def OAI.ContinuumCoulomb.MediatorIteration.secondPaths line 130
  29. def OAI.ContinuumCoulomb.MediatorIteration.retainedCentral line 134
  30. def OAI.ContinuumCoulomb.MediatorIteration.thirdCentral line 137
  31. def OAI.ContinuumCoulomb.MediatorIteration.thirdSpokes line 141
  32. def OAI.ContinuumCoulomb.MediatorIteration.finalGraph line 147
  33. def OAI.ContinuumCoulomb.MediatorIteration.firstGraph line 153
  34. def OAI.ContinuumCoulomb.MediatorIteration.secondGraph line 156
  35. theorem OAI.ContinuumCoulomb.MediatorIteration.final_vertex_count line 160
  36. theorem OAI.ContinuumCoulomb.MediatorIteration.final_edge_count line 163
  37. theorem OAI.ContinuumCoulomb.MediatorIteration.finalGraph_noLoops line 166
  38. theorem OAI.ContinuumCoulomb.MediatorIteration.join_weight_property line 172
  39. theorem OAI.ContinuumCoulomb.MediatorIteration.firstSpokes_bounds line 181
  40. theorem OAI.ContinuumCoulomb.MediatorIteration.secondPaths_bounds line 188
  41. theorem OAI.ContinuumCoulomb.MediatorIteration.firstCentral_weight_sum line 205
  42. theorem OAI.ContinuumCoulomb.MediatorIteration.firstCentral_bound line 209
  43. theorem OAI.ContinuumCoulomb.MediatorIteration.retainedCentral_bound line 218
  44. def OAI.ContinuumCoulomb.MediatorIteration.offset line 228
  45. theorem OAI.ContinuumCoulomb.MediatorIteration.lift_empty_matrix line 233
  46. theorem OAI.ContinuumCoulomb.MediatorIteration.family_stage_bound line 236
  47. theorem OAI.ContinuumCoulomb.MediatorIteration.first_stage line 251
  48. theorem OAI.ContinuumCoulomb.MediatorIteration.second_stage line 261
  49. theorem OAI.ContinuumCoulomb.MediatorIteration.third_stage line 275
  50. theorem OAI.ContinuumCoulomb.MediatorIteration.three_stage_bottom line 294

    Source documentation

    Three concrete rational graph stages give the promised finite-spin energy comparison, including all three exact rational scalar offsets.

    theorem three_stage_bottom {n r W G : ℕ} (F : Bonds n r) (hF : F.NoLoops)
    (hW : 0 < W) (hG : 0 < G) (hJ : ∀ e, |(F.weight e : ℝ)| ≤ W)
    (hJl : ∀ e, 1 / (W : ℝ) ≤ |(F.weight e : ℝ)|) :
    |sourceMatrixBottom (n + r * 2 + r * 2 * 2 + (r * 2 + r * 2 * 2) * 2) (finalGraph F W G).matrix +
      (offset F W G : ℝ) - sourceMatrixBottom n F.matrix| ≤ 3 / (512 * (G : ℝ)) := by
…

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

  51. theorem OAI.ContinuumCoulomb.MediatorIteration.finalGraph_positive line 311