OAI/Probability/DilutedSpin/ParameterProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.measurePreserving_parameter_refresh line 13

   Source documentation

   Refreshing a single coordinate by an independent sample preserves the entire countable parameter law. The other coordinates are not truncated.

   theorem measurePreserving_parameter_refresh {ι : Type*} [DecidableEq ι]
       (μ : ι → Measure ℝ) [∀ i, IsProbabilityMeasure (μ i)] (i : ι) :
       MeasurePreserving (fun z : (ι → ℝ) × ℝ => Function.update z.1 i z.2)
         ((Measure.infinitePi μ).prod (μ i)) (Measure.infinitePi μ) := by
   …

2. def OAI.DilutedSpinGlass.intervalParameterLaw line 58
3. lemma OAI.DilutedSpinGlass.intervalParameterLaw_probability line 60
4. lemma OAI.DilutedSpinGlass.integral_intervalParameterLaw line 68
5. lemma OAI.DilutedSpinGlass.integral_parameter_refresh line 76

   Source documentation

   A complete-parameter average is the independent refresh average.

   lemma integral_parameter_refresh {ι : Type*} [DecidableEq ι]
       (μ : ι → Measure ℝ) [∀ i, IsProbabilityMeasure (μ i)] (i : ι)
       (f : (ι → ℝ) → ℝ) (hf : Measurable f) (hi : Integrable f (Measure.infinitePi μ)) :
       (∫ z, f z ∂Measure.infinitePi μ) =
         ∫ z, ∫ u, f (Function.update z i u) ∂μ i ∂Measure.infinitePi μ := by
   …

6. lemma OAI.DilutedSpinGlass.parameter_average_le line 93

   Source documentation

   Uniform interval estimates with every other coordinate fixed imply the same estimate under the literal infinite product parameter law.

   lemma parameter_average_le {ι : Type*} [DecidableEq ι]
       (a b : ι → ℝ) (hab : ∀ i, a i < b i) (i : ι)
       (f : (ι → ℝ) → ℝ) (hf : Measurable f)
       (hi : Integrable f (Measure.infinitePi (fun i => intervalParameterLaw (a i) (b i))))
       {B : ℝ} (hB : ∀ z, (∫ u in a i..b i, f (Function.update z i u))/(b i-a i) ≤ B) :
       (∫ z, f z ∂Measure.infinitePi (fun i => intervalParameterLaw (a i) (b i))) ≤ B := by
   …

   Mentions: OAI.DilutedSpinGlass.intervalParameterLaw

7. lemma OAI.DilutedSpinGlass.integral_select_product line 120

   Source documentation

   Selecting one type in the complete dictionary law keeps its unmodified conditional site law. This is the scalar normalization in the Palm identity.

   lemma integral_select_product {J Z : Type*} [MeasurableSpace J] [MeasurableSingletonClass J]
       [MeasurableSpace Z] [Countable J] [Countable Z] [MeasurableSingletonClass Z]
       [DecidableEq J] (ν : Measure J) [IsProbabilityMeasure ν]
       (τ : Measure Z) [IsProbabilityMeasure τ] (j : J) (F : J × Z → ℝ)
       {B : ℝ} (hB : 0 ≤ B) (hF : ∀ x, |F x| ≤ B) :
       (∫ x, if x.1 = j then F x else 0 ∂ν.prod τ) =
         ν.real {j} * ∫ z, F (j,z) ∂τ := by
   …

8. lemma OAI.DilutedSpinGlass.integral_fresh_label line 143

   Source documentation

   Inserting with a pushed-forward site law is genuinely independent of the old reservoir. The old state law is not changed by this relabeling.

   lemma integral_fresh_label {W J Z : Type*} [MeasurableSpace W] [MeasurableSpace J]
       [MeasurableSpace Z] (ρ : Measure W) [IsProbabilityMeasure ρ]
       (τ : Measure Z) [IsProbabilityMeasure τ] (label : Z → J) (hl : Measurable label)
       (F : W × J → ℝ) (hF : Measurable F) {B : ℝ} (hb : ∀ z, |F z| ≤ B) :
       (∫ z, F z ∂ρ.prod (τ.map label)) = ∫ w, ∫ z, F (w,label z) ∂τ ∂ρ := by
   …