OAI/Probability/DilutedSpin/PerturbedSizeCoupling.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DilutedSpinGlass.SizeCoupling.perturbedMean line 18

    Source documentation

    Total (unnormalized) pressure of the literal countable reservoir. The entropy restores the counting-spin partition function from uniform spins.

    noncomputable def perturbedMean (μ : Measure X) (ξ : Measure Y) (ν : Measure I)
    {p r N : ℕ} [NeZero N] (theta : X → InteractionSample p) (field : Y → ℝ)
    (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
    (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ) (u v : ℝ≥0) : ℝ :=
…

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

  2. theorem OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_size_rate_coupling line 24
  3. def OAI.DilutedSpinGlass.scoreRate line 74
  4. lemma OAI.DilutedSpinGlass.scoreScale_mono line 76
  5. lemma OAI.DilutedSpinGlass.scoreScale_succ_sub_le line 80
  6. theorem OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_uniform_increment line 100

    Source documentation

    The uniform lower and upper increment envelope needed by deterministic parameter selection. Dependence on the entire dictionary and on all priors has cancelled; the original uncapped N^(3/4) scale is used.

    theorem perturbedMean_uniform_increment (μ : 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 : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hθ : ∀ x σ, |(theta x).1 σ| ≤ C) (hh : ∀ y, |field y| ≤ H)
    (hψ : ∀ i σ a, |Real.log (ψ i σ a)| ≤ D) (α : ℝ≥0) :
    |perturbedMean (N := N+1) μ ξ ν theta field Q m ψ (α*(N+1)) (scoreRate (N+1))-
…

    Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.perturbedMean, OAI.DilutedSpinGlass.scoreRate