OAI/Probability/DilutedSpin/Perturbations.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.KernelTower.perturbLog line 14

   Source documentation

   Actual log weight after a finite family of perturbations of one type. The base includes the physical Hamiltonian and every other fixed type.

   noncomputable def perturbLog {L n : ℕ} (base : FinitePath Ω L → ℝ)
       (D E : Fin n → FinitePath Ω L → ℝ) (t u : ℝ) (y : FinitePath Ω L) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.FinitePath

2. def OAI.DilutedSpinGlass.KernelTower.perturbScore line 18
3. def OAI.DilutedSpinGlass.KernelTower.perturbCurvature line 22
4. theorem OAI.DilutedSpinGlass.KernelTower.perturb_factor_lower line 27
5. theorem OAI.DilutedSpinGlass.KernelTower.hasDerivAt_perturbLog line 37
6. theorem OAI.DilutedSpinGlass.KernelTower.hasDerivAt_perturbScore line 47
7. theorem OAI.DilutedSpinGlass.KernelTower.perturb_fraction_bound line 63
8. theorem OAI.DilutedSpinGlass.KernelTower.perturbScore_bound line 73
9. theorem OAI.DilutedSpinGlass.KernelTower.perturbCurvature_bounds line 84
10. theorem OAI.DilutedSpinGlass.KernelTower.perturb_thermal_variance line 99
11. def OAI.DilutedSpinGlass.KernelTower.correctedPerturbLog line 137

    Source documentation

    The manuscript's random convex correction, still before any root expectation is taken.

    noncomputable def correctedPerturbLog {L n : ℕ} (T : KernelTower Ω L) (m : Fin L → ℝ)
        (base : FinitePath Ω L → ℝ) (D E : Fin n → FinitePath Ω L → ℝ) (t u : ℝ) : ℝ :=
    …

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

12. def OAI.DilutedSpinGlass.KernelTower.correctedPerturbScore line 141
13. theorem OAI.DilutedSpinGlass.KernelTower.hasDerivAt_correctedPerturbLog line 145
14. theorem OAI.DilutedSpinGlass.KernelTower.hasDerivAt_correctedPerturbScore line 162
15. theorem OAI.DilutedSpinGlass.KernelTower.correctedPerturbLog_convex line 179
16. theorem OAI.DilutedSpinGlass.FiniteLaw.measurable_tilt_expect line 212
17. theorem OAI.DilutedSpinGlass.FiniteLaw.mean_absolute_deviation_sq line 222

    Source documentation

    Conditional absolute score fluctuations are controlled by their exact conditional variance; all randomness is still in the tilted path law.

    theorem mean_absolute_deviation_sq (P : FiniteLaw Ω) (f : Ω → ℝ) :
        (P.expect (fun x => |f x-P.expect f|))^2 ≤ P.covariance f f := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw

18. theorem OAI.DilutedSpinGlass.KernelTower.measurable_path_expect line 234
19. theorem OAI.DilutedSpinGlass.KernelTower.continuousOn_perturbLog line 248
20. theorem OAI.DilutedSpinGlass.KernelTower.continuousOn_perturbScore line 261
21. def OAI.DilutedSpinGlass.KernelTower.thermalDefect line 273

    Source documentation

    The L1 thermal defect for the literal score of all selected marks.

    noncomputable def thermalDefect {L n : ℕ} (T : KernelTower Ω L) (m : Fin L → ℝ)
        (base : FinitePath Ω L → ℝ) (D E : Fin n → FinitePath Ω L → ℝ) (t u : ℝ) : ℝ :=
    …

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

22. theorem OAI.DilutedSpinGlass.KernelTower.thermalDefect_nonneg line 279
23. theorem OAI.DilutedSpinGlass.KernelTower.continuousOn_thermalDefect line 285
24. theorem OAI.DilutedSpinGlass.KernelTower.measurable_perturbLog line 302
25. theorem OAI.DilutedSpinGlass.KernelTower.measurable_perturbScore line 315
26. theorem OAI.DilutedSpinGlass.KernelTower.measurable_thermalDefect line 324
27. theorem OAI.DilutedSpinGlass.sq_intervalIntegral_le line 342
28. theorem OAI.DilutedSpinGlass.KernelTower.perturb_thermal_absolute line 377
29. theorem OAI.DilutedSpinGlass.poisson_family_average_sq line 418
30. theorem OAI.DilutedSpinGlass.poisson_thermal_absolute line 456

    Source documentation

    The actual thermal estimate after both independent root averaging and Poisson averaging, allowing the whole mark alphabet/tower to depend on the count.

    theorem poisson_thermal_absolute
        {X Ω : ℕ → Type} [∀ n, MeasurableSpace (X n)] [∀ n, Fintype (Ω n)]
        (ν : ∀ n, Measure (X n)) [∀ n, IsProbabilityMeasure (ν n)] (r : ℝ≥0)
        (L : ℕ) (T : ∀ n, KernelTower (Ω n) L) (m : Fin L → ℝ)
        (base : ∀ n, X n → FinitePath (Ω n) L → ℝ)
        (D E : ∀ n, X n → Fin n → FinitePath (Ω n) L → ℝ)
        (hb : ∀ n y, Measurable (fun x => base n x y))
        (hD : ∀ n q y, Measurable (fun x => D n x q y))
        (hE : ∀ n q y, Measurable (fun x => E n x q y))
        (hDb : ∀ n x q y, |D n x q y| ≤ 1)
        (hEb : ∀ n x q y, |E n x q y| ≤ 1)
        {t a b c : ℝ} (ht : |t| ≤ 1/4) (hab : a < b) (hc : 0 < c)
    …

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