Stat.Finite­Rao­Blackwell.Poisson.Finite­Partition.Nested­Event­Moment

theorem finitePoisson_nestedEvent_factorialMoment (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (A B : Set X) (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : A ⊆ B) (v : ℕ) (hv : 1 ≤ v) : (∫ s, weightedFactorial A B v s ∂finitePoissonSampleLaw P lam) = (lam : ℝ) ^ v * (P A).toReal * (P B).toReal ^ (v - 1) := by /- Disintegrate along the measurable sample count. On fibre n, use integral_weightedFactorial_countFibre. The resulting Poisson sum is the scalar descFactorial moment. The integrability lemma licenses countable integral interchange. -/ let μ := finitePoissonSampleLaw P lam let S : ℕ → Set (FiniteSample X) := fun n => FiniteSample.count ⁻¹' ({n} : Set ℕ) have hdis : Pairwise (onFun Disjoint S) := by intro i j hij apply Set.disjoint_left.mpr intro s hi hj exact hij (hi.symm.trans hj) have hcover : (⋃ n, S n) = univ := by ext s simp [S] have hsum : μ = Measure.sum (fun n => μ.restrict (S n)) := by calc μ = μ.restrict univ := (Measure.restrict_univ).symm _ = μ.restrict (⋃ n, S n) := by rw [hcover] _ = Measure.sum (fun n => μ.restrict (S n)) := Measure.restrict_iUnion hdis (fun n => measurable_finiteSample_count (MeasurableSet.singleton n)) have hf : Integrable (weightedFactorial A B v) μ := integrable_weightedFactorial P lam A B hA hB hAB v hv have hscalar : Integrable (fun n : ℕ => (n.descFactorial v : ℝ)) (poissonMeasure lam) := Causalean.Stat.Concentration.Poisson.poisson_descFactorial_integrable lam v have hs : Summable (fun n : ℕ => ((poissonMeasure lam) {n}).toReal * (n.descFactorial v : ℝ)) := by rw [← Measure.sum_smul_dirac (poissonMeasure lam)] at hscalar simpa using hscalar.summable_of_dirac calc (∫ s, weightedFactorial A B v s ∂μ) = ∑' n, ∫ s, weightedFactorial A B v s ∂μ.restrict (S n) := by conv_lhs => rw [hsum] exact integral_sum_measure (hsum ▸ hf) _ = ∑' n, (((poissonMeasure lam) {n}).toReal * (n.descFactorial v : ℝ)) * ((P A).toReal * (P B).toReal ^ (v - 1)) := by congr 1 funext n rw [integral_weightedFactorial_countFibre P lam A B hA hB hAB v n hv] ring _ = (∑' n, ((poissonMeasure lam) {n}).toReal * (n.descFactorial v : ℝ)) * ((P A).toReal * (P B).toReal ^ (v - 1)) := hs.tsum_mul_right _ _ = (lam : ℝ) ^ v * (P A).toReal * (P B).toReal ^ (v - 1) := by have hm := poisson_descFactorial_moment lam v rw [integral_countable hscalar] at hm have hseries : (∑' n, ((poissonMeasure lam) {n}).toReal * (n.descFactorial v : ℝ)) = (lam : ℝ) ^ v := by simpa only [measureReal_def, smul_eq_mul] using hm rw [hseries] ring

theorem weightedFactorial_eq_injectiveTupleSum (A B : Set X) (hAB : A ⊆ B) (v n : ℕ) (hv : 1 ≤ v) (x : Fin n → X) : weightedFactorial A B v (fixedSizeEmbed n x) = ∑ t ∈ injectiveTuples v n, nestedEventKernel A B v hv (fun j => x (t j)) := by classical cases v with | zero => omega | succ k => let sA : Finset (Fin n) := Finset.univ.filter (fun i => x i ∈ A) let sB : Finset (Fin n) := Finset.univ.filter (fun i => x i ∈ B) have htail (t : Fin (k + 1) → Fin n) : (∀ j : Fin (k + 1), j.val ≠ 0 → x (t j) ∈ B) ↔ ∀ j : Fin k, x (t j.succ) ∈ B := by constructor · intro h j exact h j.succ (by simp) · intro h j hj induction j using Fin.cases with | zero => exact False.elim (hj rfl) | succ a => exact h a have hinner (i : Fin n) : (∑ t ∈ (injectiveTuples (k + 1) n).filter (fun t => t 0 = i), nestedEventKernel A B (k + 1) hv (fun j => x (t j))) = if x i ∈ A then ((sB.card - 1).descFactorial k : ℝ) else 0 := by by_cases hiA : x i ∈ A · have hiB : i ∈ sB := Finset.mem_filter.mpr ⟨Finset.mem_univ _, hAB hiA⟩ simp only [hiA, ite_true] have hpoint : ∀ t ∈ (injectiveTuples (k + 1) n).filter (fun t => t 0 = i), nestedEventKernel A B (k + 1) hv (fun j => x (t j)) = if ∀ j : Fin k, x (t j.succ) ∈ B then 1 else 0 := by intro t ht have hfirst : t 0 = i := (Finset.mem_filter.mp ht).2 change (if x (t 0) ∈ A ∧ (∀ j : Fin (k + 1), j.val ≠ 0 → x (t j) ∈ B) then (1 : ℝ) else 0) = _ simp only [hfirst, hiA, true_and, htail] rw [Finset.sum_congr rfl hpoint] rw [Finset.sum_boole] have hfilt : ((injectiveTuples (k + 1) n).filter (fun t => t 0 = i)).filter (fun t => ∀ j : Fin k, x (t j.succ) ∈ B) = (injectiveTuples (k + 1) n).filter (fun t => t 0 = i ∧ ∀ j : Fin k, t j.succ ∈ sB) := by ext t simp [sB, Finset.filter_filter] rw [hfilt, card_injectiveTuples_first k n sB i hiB] · simp only [hiA, ite_false] apply Finset.sum_eq_zero intro t ht have hfirst : t 0 = i := (Finset.mem_filter.mp ht).2 simp [nestedEventKernel, hfirst, hiA] have hsum : (∑ t ∈ injectiveTuples (k + 1) n, nestedEventKernel A B (k + 1) hv (fun j => x (t j))) = ∑ i : Fin n, if x i ∈ A then ((sB.card - 1).descFactorial k : ℝ) else 0 := by calc _ = ∑ i : Fin n, ∑ t ∈ (injectiveTuples (k + 1) n).filter (fun t => t 0 = i), nestedEventKernel A B (k + 1) hv (fun j => x (t j)) := (Finset.sum_fiberwise (injectiveTuples (k + 1) n) (fun t => t 0) (fun t => nestedEventKernel A B (k + 1) hv (fun j => x (t j)))).symm _ = _ := by simp only [hinner] rw [hsum] change (sA.card : ℝ) * ((sB.card - 1).descFactorial k : ℝ) = ∑ i : Fin n, if x i ∈ A then ((sB.card - 1).descFactorial k : ℝ) else 0 rw [← Finset.sum_filter] change (sA.card : ℝ) * ((sB.card - 1).descFactorial k : ℝ) = ∑ _i ∈ sA, ((sB.card - 1).descFactorial k : ℝ) simp

theorem weightedFactorial_nonneg_le_countFactorial (A B : Set X) (hAB : A ⊆ B) (v : ℕ) (hv : 1 ≤ v) (s : FiniteSample X) : 0 ≤ weightedFactorial A B v s ∧ weightedFactorial A B v s ≤ (s.count.descFactorial v : ℝ) := by classical rcases s with ⟨n, x⟩ change 0 ≤ weightedFactorial A B v (fixedSizeEmbed n x) ∧ weightedFactorial A B v (fixedSizeEmbed n x) ≤ (n.descFactorial v : ℝ) rw [weightedFactorial_eq_injectiveTupleSum A B hAB v n hv x] have hkernel (t : Fin v → Fin n) : 0 ≤ nestedEventKernel A B v hv (fun j => x (t j)) ∧ nestedEventKernel A B v hv (fun j => x (t j)) ≤ 1 := by unfold nestedEventKernel split_ifs <;> norm_num constructor · exact Finset.sum_nonneg fun t ht => hkernel t |>.1 · calc (∑ t ∈ injectiveTuples v n, nestedEventKernel A B v hv (fun j => x (t j))) ≤ ∑ _t ∈ injectiveTuples v n, (1 : ℝ) := by apply Finset.sum_le_sum intro t ht exact (hkernel t).2 _ = (n.descFactorial v : ℝ) := by simp [injectiveTuples_card_eq_descFactorial]

theorem integral_weightedFactorial_countFibre (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (A B : Set X) (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : A ⊆ B) (v n : ℕ) (hv : 1 ≤ v) : (∫ s, weightedFactorial A B v s ∂ (finitePoissonSampleLaw P lam).restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ))) = ((poissonMeasure lam) ({n} : Set ℕ)).toReal * (n.descFactorial v : ℝ) * (P A).toReal * (P B).toReal ^ (v - 1) := by rw [finitePoissonSampleLaw_restrict_count_eq, integral_smul_measure] rw [integral_map (measurable_fixedSizeEmbed n).aemeasurable (measurable_weightedFactorial A B hA hB v).aestronglyMeasurable] rw [integral_weightedFactorial_fixedCount P A B hA hB hAB v n hv] simp only [smul_eq_mul] ring

theorem integral_weightedFactorial_fixedCount (P : Measure X) [IsProbabilityMeasure P] (A B : Set X) (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : A ⊆ B) (v n : ℕ) (hv : 1 ≤ v) : (∫ x : Fin n → X, weightedFactorial A B v (fixedSizeEmbed n x) ∂Measure.pi (fun _ : Fin n => P)) = (n.descFactorial v : ℝ) * (P A).toReal * (P B).toReal ^ (v - 1) := by /- Rewrite by weightedFactorial_eq_injectiveTupleSum. For each injective t : Fin v → Fin n, the coordinate projection x ↦ fun j => x (t j) pushes the finite product law P^n to P^v. Prove this using `iIndepFun_pi` and `iIndepFun_iff_map_fun_eq_pi_map` (or a finite-product marginal theorem); then transfer integrability and the kernel integral. Sum over injectiveTuples and use injectiveTuples_card_eq_descFactorial. This also handles n < v because the tuple finset is empty and n.descFactorial v = 0. The IIDSample theorem in OrderM.Variance is a useful analogue but its sample interface is indexed by ℕ, unlike this finite product fibre. -/ classical let μ : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => P) let ν : Measure (Fin v → X) := Measure.pi (fun _ : Fin v => P) let f (t : Fin v → Fin n) (x : Fin n → X) : Fin v → X := fun j => x (t j) have hproj (t : Fin v → Fin n) (ht : Injective t) : μ.map (f t) = ν := by have hind : iIndepFun (fun j : Fin v => Function.eval (t j)) μ := (iIndepFun_pi (X := fun _ : Fin n => id) (fun _ => measurable_id.aemeasurable)).precomp ht have hmap := (iIndepFun_iff_map_fun_eq_pi_map (fun j : Fin v => (measurable_pi_apply (t j)).aemeasurable)).mp hind calc μ.map (f t) = Measure.pi (fun j : Fin v => μ.map (Function.eval (t j))) := hmap _ = ν := by congr 1 funext j exact (measurePreserving_eval (fun _ : Fin n => P) (t j)).map_eq have hterm (t : Fin v → Fin n) (ht : t ∈ injectiveTuples v n) : (∫ x : Fin n → X, nestedEventKernel A B v hv (f t x) ∂μ) = (P A).toReal * (P B).toReal ^ (v - 1) := by have hti : Injective t := by simpa [injectiveTuples] using ht have hm : Measurable (f t) := measurable_pi_lambda _ (fun j => measurable_pi_apply (t j)) have hk := (integrable_nestedEventKernel P A B hA hB v hv).aestronglyMeasurable calc _ = ∫ y : Fin v → X, nestedEventKernel A B v hv y ∂(μ.map (f t)) := (integral_map hm.aemeasurable (by simpa [hproj t hti, ν] using hk)).symm _ = _ := by rw [hproj t hti]; exact integral_nestedEventKernel P A B hA hB v hv rw [show (fun x : Fin n → X => weightedFactorial A B v (fixedSizeEmbed n x)) = (fun x => ∑ t ∈ injectiveTuples v n, nestedEventKernel A B v hv (f t x)) by funext x exact weightedFactorial_eq_injectiveTupleSum A B hAB v n hv x] rw [integral_finsetSum] · have hsum : (∑ t ∈ injectiveTuples v n, ∫ x : Fin n → X, nestedEventKernel A B v hv (f t x) ∂μ) = ∑ t ∈ injectiveTuples v n, (P A).toReal * (P B).toReal ^ (v - 1) := by apply Finset.sum_congr rfl intro t ht exact hterm t ht rw [show Measure.pi (fun _ : Fin n => P) = μ by rfl, hsum] simp only [Finset.sum_const, nsmul_eq_mul] rw [injectiveTuples_card_eq_descFactorial] ring · intro t ht have hti : Injective t := by simpa [injectiveTuples] using ht have hm : Measurable (f t) := measurable_pi_lambda _ (fun j => measurable_pi_apply (t j)) have hk := integrable_nestedEventKernel P A B hA hB v hv have hkmap : Integrable (nestedEventKernel A B v hv) (μ.map (f t)) := by rw [hproj t hti] exact hk exact (integrable_map_measure hkmap.aestronglyMeasurable hm.aemeasurable).mp hkmap