OAI/Probability/DilutedSpin/FullThermalAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.full_selected_thermal_average line 16
2. def OAI.DilutedSpinGlass.KernelTower.prefixEnergyAt line 66

   Source documentation

   The squared spatial covariance density under the conditional continuation law after a prefix of length d. This version allows the fixed physical height.

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

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

3. lemma OAI.DilutedSpinGlass.KernelTower.prefixEnergyAt_nonneg line 72
4. lemma OAI.DilutedSpinGlass.KernelTower.prefixEnergyAt_eq line 81
5. lemma OAI.DilutedSpinGlass.KernelTower.prefix_three_copy_bound_at line 88