OAI/Probability/DilutedSpin/FinitePiInjective.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.FiniteLaw.injectionFactor line 12
2. lemma OAI.DilutedSpinGlass.FiniteLaw.injectionFactor_apply line 17
3. lemma OAI.DilutedSpinGlass.FiniteLaw.injectionFactor_outside line 31
4. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_injective_product line 40

   Source documentation

   A finite family of distinct child coordinates has the corresponding product law, regardless of the unused coordinates in the full old tree.

   lemma expect_pi_injective_product (P : (j : κ) → FiniteLaw (α j))
       (e : ι → κ) (he : Function.Injective e) (g : (i : ι) → α (e i) → ℝ) :
       (pi P).expect (fun x => ∏ i, g i (x (e i))) = ∏ i, (P (e i)).expect (g i) := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.expect

5. lemma OAI.DilutedSpinGlass.FiniteLaw.product_point_indicator line 56
6. lemma OAI.DilutedSpinGlass.FiniteLaw.finite_indicator_expansion line 67
7. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_injective line 76