OAI/Analysis/MutuallyUnbiased/Moments/SamplingAverage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.Sampling.unused_card line 16
2. theorem OAI.MUB6.Sampling.embedding_succ_card line 24
3. theorem OAI.MUB6.Sampling.sum_dropFirst line 30
4. theorem OAI.MUB6.Sampling.average_dropFirst line 42

   Source documentation

   Deleting a coordinate of a uniform injection leaves a uniform injection.

   theorem average_dropFirst {p n : ℕ} (hp : p < n) (f : (Fin p ↪ Fin n) → ℝ) :
       average (fun e : Fin (p + 1) ↪ Fin n => f (dropFirst e)) = average f := by
   …

   Mentions: OAI.MUB6.average, OAI.MUB6.Sampling.dropFirst

5. theorem OAI.MUB6.Sampling.average_contraction line 54

   Source documentation

   The normalized counting identity used for an order-one contraction. At most n rows are sampled; the saturated boundary case is separate.

   theorem average_contraction {p n : ℕ} (hp : p < n)
       (f : (Fin p ↪ Fin n) → Fin n → ℝ) (h : ∀ e, ∑ b, f e b = 0) :
       ((n - p : ℕ) : ℝ) *
         average (fun e : Fin (p + 1) ↪ Fin n => f (dropFirst e) (e 0)) +
         (∑ j : Fin p, average (fun e : Fin p ↪ Fin n => f e (e j))) = 0 := by
   …

   Mentions: OAI.MUB6.average, OAI.MUB6.Sampling.dropFirst

6. theorem OAI.MUB6.Sampling.saturated_average_contraction line 72

   Source documentation

   At saturation the old labels exhaust the population, so only the occupied contractions occur. This statement never defines a seven-row moment.

   theorem saturated_average_contraction (n : ℕ)
       (f : (Fin n ↪ Fin n) → Fin n → ℝ) (h : ∀ e, ∑ b, f e b = 0) :
       (∑ j : Fin n, average (fun e : Fin n ↪ Fin n => f e (e j))) = 0 := by
   …

   Mentions: OAI.MUB6.average