OAI/Probability/DilutedSpin/SelectorPolarization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory line 12

   Source documentation

   The exact signed constrained history sum for an anchored old tree.

   noncomputable def constrainedHistory {n k : ℕ} {R : Type} [Fintype R] [DecidableEq R]
       (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (a b : R → Option (Fin k)) (d : R → Fin n)
       (spinColor : Option (Fin k) → FinitePath Ω n → ℝ)
       (S : PrescribedTree n) (anchor : S.Leaf) (f : Sample Ω S → ℝ) : ℝ := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample

2. theorem OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory_polarization line 27

   Source documentation

   Polarization and the actual tree mark selector identify the constrained history sum with diagonal canceled-anchor coefficients. The factorial cancels exactly, leaving k^k/2^k times the signed finite sum of Taylor coefficients.

   theorem constrainedHistory_polarization {n k : ℕ} {R : Type} [Fintype R] [DecidableEq R]
       (hk : 0 < k) (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
       (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
       (a b : R → Option (Fin k)) (d : R → Fin n)
       (spinColor : Option (Fin k) → FinitePath Ω n → ℝ)
       (S : PrescribedTree n) (anchor : S.Leaf) (f : Sample Ω S → ℝ) :
       let T' := KernelTower.prod n T (markPrior n (fun _ => FiniteLaw.pi (fun _ : R => MarkSelector.rademacher)))
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.prod, OAI.DilutedSpinGlass.markPrior, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.MarkSelector.rademacher