OAI/Probability/DilutedSpin/FiniteProducts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_split line 13

   Source documentation

   Fubini at an arbitrary coordinate, retaining dependent finite sample types.

   theorem expect_pi_split {ι : Type*} [Fintype ι] [DecidableEq ι]
       {α : ι → Type*} [∀ i, Fintype (α i)] (Q : (i : ι) → FiniteLaw (α i))
       (i : ι) (H : ((i : ι) → α i) → ℝ) :
       (pi Q).expect H = (Q i).expect (fun a =>
         (pi (fun j : {j // j ≠ i} => Q j)).expect
           (fun rest => H ((Equiv.piSplitAt i α).symm (a,rest)))) := by
   …

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

2. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_cons line 48

   Source documentation

   Split off the new first child at a root attachment.

   theorem expect_pi_cons {n : ℕ} {α : Fin (n+1) → Type*} [∀ i, Fintype (α i)]
       (Q : (i : Fin (n+1)) → FiniteLaw (α i)) (H : ((i : Fin (n+1)) → α i) → ℝ) :
       (pi Q).expect H = (Q 0).expect (fun a =>
         (pi (fun j : Fin n => Q j.succ)).expect (fun rest => H (Fin.cons a rest))) := by
   …

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

3. def OAI.DilutedSpinGlass.FiniteLaw.delta line 70
4. theorem OAI.DilutedSpinGlass.FiniteLaw.delta_pi line 74
5. theorem OAI.DilutedSpinGlass.FiniteLaw.expand_pi line 90
6. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_expand line 97
7. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_weighted_map line 121

   Source documentation

   Tensorization of arbitrary signed one-coordinate changes. This permits inserting a marked new branch at a single child without assuming the test factors across the old children.

   theorem expect_pi_weighted_map {ι : Type*} [Fintype ι] [DecidableEq ι]
       {α β : ι → Type*} [∀ i, Fintype (α i)] [∀ i, Fintype (β i)]
       (P : (i : ι) → FiniteLaw (α i)) (Q : (i : ι) → FiniteLaw (β i))
       (φ : (i : ι) → α i → β i) (w : (i : ι) → α i → ℝ) (v : (i : ι) → β i → ℝ)
       (h : ∀ i (g : β i → ℝ), (P i).expect (fun x => w i x * g (φ i x)) =
         (Q i).expect (fun y => v i y * g y)) (H : ((i : ι) → β i) → ℝ) :
       (pi P).expect (fun x => H (fun i => φ i (x i)) * ∏ i, w i (x i)) =
         (pi Q).expect (fun y => H y * ∏ i, v i (y i)) := by
   …

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

8. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_marginal line 141