OAI/Probability/DilutedSpin/ActualNegligible.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.KernelTower.prefixCovarianceEnergy line 15

   Source documentation

   Conditional covariance density at the branching depth, averaged over the actual shared prefix kernels.

   noncomputable def prefixCovarianceEnergy (h : ℕ) : (d : ℕ) →
       KernelTower Ω (h+1+d) → (FinitePath Ω (h+1+d) → Fin N → ℝ) → ℝ
     | 0, T, X => (law (h+1) T).covarianceEnergy X
     | d+1, T, X => T.1.expect (fun z => prefixCovarianceEnergy h d (T.2 z) (fun y => X (z,y)))

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law

2. def OAI.DilutedSpinGlass.KernelTower.tripleExpect line 20
3. lemma OAI.DilutedSpinGlass.KernelTower.prefixCovarianceEnergy_nonneg line 26
4. lemma OAI.DilutedSpinGlass.KernelTower.prefix_three_copy_bound line 34

   Source documentation

   The first genuinely new branch at the divergence vertex controls squared conditional covariance, including the zero-site normalization endpoint.

   lemma prefix_three_copy_bound (h d : ℕ) (T : KernelTower Ω (h+1+d))
       (X : FinitePath Ω (h+1+d) → Fin N → ℝ) :
       2*prefixCovarianceEnergy h d T X ≤ tripleExpect h d T
         (fun x y z => (FiniteLaw.dot (X x) (X y)-FiniteLaw.dot (X x) (X z))^2) := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.prefixCovarianceEnergy, OAI.DilutedSpinGlass.KernelTower.tripleExpect, OAI.DilutedSpinGlass.FiniteLaw.dot

5. lemma OAI.DilutedSpinGlass.PrescribedTree.fork_fresh_joint line 57
6. theorem OAI.DilutedSpinGlass.PrescribedTree.fork_three_joint line 91

   Source documentation

   Exact conditional independence of the three ACTUAL continuations at d, not an independence hypothesis added to the eventual Gibbs reservoir.

   theorem fork_three_joint (h d : ℕ) (T : KernelTower Ω (h+1+d))
       (F : FinitePath Ω (h+1+d) → FinitePath Ω (h+1+d) → FinitePath Ω (h+1+d) → ℝ) :
       ((grow (fork h 2 d) (forkVertex h 2 d)).sampleLaw T).expect
         (fun x => F
           ((fork h 2 d).pathAt (forkLeaf h 2 d 0) (oldSample (fork h 2 d) (forkVertex h 2 d) x))
           ((fork h 2 d).pathAt (forkLeaf h 2 d 1) (oldSample (fork h 2 d) (forkVertex h 2 d) x))
           (newPath (fork h 2 d) (forkVertex h 2 d) x)) = KernelTower.tripleExpect h d T F := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.fork, OAI.DilutedSpinGlass.PrescribedTree.forkVertex, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.forkLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldSample, OAI.DilutedSpinGlass.PrescribedTree.newPath, OAI.DilutedSpinGlass.KernelTower.tripleExpect

7. lemma OAI.DilutedSpinGlass.SizeCoupling.countedMean_eq_pi line 118
8. lemma OAI.DilutedSpinGlass.SizeCoupling.spinFieldIntegral_close line 143
9. lemma OAI.DilutedSpinGlass.SizeCoupling.spinDisorderIntegral_close line 168
10. theorem OAI.DilutedSpinGlass.SizeCoupling.actual_countedMean_close line 198
11. theorem OAI.DilutedSpinGlass.SizeCoupling.actual_perturbedMean_close line 217
12. def OAI.DilutedSpinGlass.PrescribedTree.forkAt line 271

    Source documentation

    Two independent branches at the designated physical height; all other levels are unary. The height stays fixed, avoiding transports of spin paths.

    def forkAt : (n d : ℕ) → d < n → PrescribedTree n
      | 0, _, hd => False.elim (Nat.not_lt_zero _ hd)
      | n+1, 0, _ => .node 2 (fun _ => single n)
      | n+1, d+1, hd => .node 1 (fun _ => forkAt n d (Nat.lt_of_succ_lt_succ hd))

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.single

13. def OAI.DilutedSpinGlass.PrescribedTree.forkAtLeaf line 276
14. def OAI.DilutedSpinGlass.PrescribedTree.forkAtVertex line 281
15. lemma OAI.DilutedSpinGlass.PrescribedTree.forkAtLeaf_surjective line 286
16. lemma OAI.DilutedSpinGlass.PrescribedTree.forkAt_split line 303
17. lemma OAI.DilutedSpinGlass.PrescribedTree.forkAt_fresh line 314
18. lemma OAI.DilutedSpinGlass.PrescribedTree.forkAt_gamma line 325
19. lemma OAI.DilutedSpinGlass.PrescribedTree.forkAt_unique line 336