OAI/Probability/DilutedSpin/ScheduledRelativeCharge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.PrescribedTree.partialKappa_ratio_bijective line 11
2. theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_relative_charge line 28

   Source documentation

   Exact grid-power cancellation for the actual delayed scheduled target, with the canonical full-to-protected-pair kappa ratio.

   theorem scheduled_relative_charge (H r d : ℕ) (k : ℕ+) (a : α)
       (C : Fin k → ReducedTopology) (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
       (Q : α → Fin (H+1+1+r+1+d)) (η : ℝ) (hη : 0<η)
       (heval : η≤((d+r+2:ℕ):ℝ)/((H+1+1+r+1+d:ℕ):ℝ)) :
       let L := H+1+1+r+1+d
   …

   Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex