OAI/Probability/DilutedSpin/CountedSteps.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.selectedFactor line 16

   Source documentation

   Vary only the selected type, not the entire countable reservoir.

   noncomputable def selectedFactor (sel : I → Bool)
       (fixed D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
       (t u : ℝ) (i : I) (x : FinitePath Ω L) (y : FinitePath (A i) L) : ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.FinitePath

2. def OAI.DilutedSpinGlass.HeterogeneousMarks.otherLog line 21
3. def OAI.DilutedSpinGlass.HeterogeneousMarks.selectedCoefficient line 26
4. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.selectedCoefficient_bound line 31
5. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.selected_perturbLog_eq line 42

   Source documentation

   Every unselected term remains in the same log weight and the same finite mark prior. This is an identity, not a distributional truncation.

   theorem selected_perturbLog_eq (base : FinitePath Ω L → ℝ) (roots : Fin n → I)
       (sel : I → Bool) (fixed D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
       (t u : ℝ) :
       KernelTower.perturbLog (otherLog base roots sel fixed)
         (selectedCoefficient roots sel D) (selectedCoefficient roots sel E) t u =
         logWeight base roots (selectedFactor sel fixed D E t u) := by
   …

   Mentions: OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.perturbLog, OAI.DilutedSpinGlass.HeterogeneousMarks.otherLog, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedCoefficient, OAI.DilutedSpinGlass.HeterogeneousMarks.logWeight, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedFactor

6. def OAI.DilutedSpinGlass.HeterogeneousMarks.selectedScore line 58
7. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.corrected_log_eq line 66
8. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.corrected_score_eq line 76
9. def OAI.DilutedSpinGlass.SizeCoupling.fieldMean line 101
10. lemma OAI.DilutedSpinGlass.SizeCoupling.fieldMean_bound line 109
11. lemma OAI.DilutedSpinGlass.SizeCoupling.measurable_fieldMean line 120
12. lemma OAI.DilutedSpinGlass.SizeCoupling.integrable_spinMean line 132
13. theorem OAI.DilutedSpinGlass.SizeCoupling.countedMean_interaction_step line 149

    Source documentation

    Count insertion of the original independent physical interaction sample.

    theorem countedMean_interaction_step (μ : Measure X) [IsProbabilityMeasure μ]
        (ξ : Measure Y) [IsProbabilityMeasure ξ] (ν : Measure I) [IsProbabilityMeasure ν]
        {p r N : ℕ} [NeZero N] (theta : X → InteractionSample p) (field : Y → ℝ)
        (hθm : ∀ σ, Measurable (fun x => (theta x).1 σ)) (hhm : Measurable field)
        (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
        (hm : ∀ j, 0 < m j) (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ)
        {C H D : ℝ} (hθ : ∀ x σ, |(theta x).1 σ| ≤ C) (hh : ∀ y, |field y| ≤ H)
        (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) (k l : ℕ) :
        |countedMean (N := N) μ ξ ν theta field Q m ψ (k+1) l-
    …

    Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.countedMean

14. theorem OAI.DilutedSpinGlass.SizeCoupling.countedMean_mark_step line 195

    Source documentation

    Count insertion draws the original countable dictionary type; its entire finite mark alphabet and all level priors are kept.

    theorem countedMean_mark_step (μ : Measure X) [IsProbabilityMeasure μ]
        (ξ : Measure Y) [IsProbabilityMeasure ξ] (ν : Measure I) [IsProbabilityMeasure ν]
        {p r N : ℕ} [NeZero N] (theta : X → InteractionSample p) (field : Y → ℝ)
        (hθm : ∀ σ, Measurable (fun x => (theta x).1 σ)) (hhm : Measurable field)
        (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
        (hm : ∀ j, 0 < m j) (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ)
        {C H D : ℝ} (hθ : ∀ x σ, |(theta x).1 σ| ≤ C) (hh : ∀ y, |field y| ≤ H)
        (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) (k l : ℕ) :
        |countedMean (N := N) μ ξ ν theta field Q m ψ k (l+1)-
    …

    Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.countedMean

15. lemma OAI.DilutedSpinGlass.poisson_abs_mean_le line 249
16. def OAI.DilutedSpinGlass.twoPoissonMean line 260
17. lemma OAI.DilutedSpinGlass.twoPoisson_inner_integrable line 263
18. lemma OAI.DilutedSpinGlass.twoPoisson_abs_mean_le line 271
19. lemma OAI.DilutedSpinGlass.twoPoissonMean_sub line 279
20. lemma OAI.DilutedSpinGlass.twoPoisson_abs_sub_le line 288
21. lemma OAI.DilutedSpinGlass.twoPoissonMean_rate_add_left line 296
22. lemma OAI.DilutedSpinGlass.twoPoissonMean_rate_add_right line 305