Mathlib.Probability.Finite­Marked­Poisson­Partition

lemma measurable_finiteSample_count : Measurable (FiniteSample.count : FiniteSample X → ℕ) := by apply measurable_to_countable' intro n change MeasurableSet ({s : FiniteSample X | s.1 = n}) rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((Sigma.mk m) ⁻¹' {s : FiniteSample X | s.1 = n}) by_cases hmn : m = n · subst m simp · convert MeasurableSet.empty using 1 ext x simp [hmn]

lemma measurable_streamToFiniteSample : Measurable (streamToFiniteSample : (ℕ × (ℕ → X)) → FiniteSample X) := by intro s hs rw [MeasurableSpace.measurableSet_iInf] at hs rw [show streamToFiniteSample ⁻¹' s = ⋃ n : ℕ, {z : ℕ × (ℕ → X) | z.1 = n} ∩ (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) ⁻¹' (fixedSizeEmbed n ⁻¹' s) by ext z simp only [mem_preimage, mem_iUnion, mem_inter_iff, mem_setOf_eq] constructor · intro hz exact ⟨z.1, rfl, hz⟩ · rintro ⟨n, hn, hz⟩ subst n exact hz] apply MeasurableSet.iUnion intro n apply MeasurableSet.inter · exact measurable_fst (measurableSet_singleton n) · have hsn : MeasurableSet (fixedSizeEmbed n ⁻¹' s) := hs n exact hsn.preimage (by fun_prop)

lemma finitePoissonSampleLaw_map_count (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) : Measure.map FiniteSample.count (finitePoissonSampleLaw P lam) = poissonMeasure lam := by unfold finitePoissonSampleLaw rw [Measure.map_map measurable_finiteSample_count measurable_streamToFiniteSample] change Measure.map fst (poissonIIDStreamLaw P lam) = poissonMeasure lam exact poissonIIDStreamLaw_map_count P lam

lemma finitePoissonSampleLaw_restrict_count_eq (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (n : ℕ) : (finitePoissonSampleLaw P lam).restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ)) = (poissonMeasure lam) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => P)) := by unfold finitePoissonSampleLaw poissonIIDStreamLaw rw [Measure.restrict_map measurable_streamToFiniteSample (measurable_finiteSample_count (X := X) (measurableSet_singleton n))] have hpre : streamToFiniteSample ⁻¹' (FiniteSample.count ⁻¹' ({n} : Set ℕ)) = ({n} : Set ℕ) ×ˢ (Set.univ : Set (ℕ → X)) := by ext z simp [streamToFiniteSample, FiniteSample.count] rw [hpre, ← Measure.restrict_prod_eq_prod_univ, Measure.restrict_singleton, Measure.prod_smul_left, Measure.map_smul, Measure.dirac_prod, Measure.map_map measurable_streamToFiniteSample (by fun_prop)] change (poissonMeasure lam) {n} • Measure.map (fixedSizeEmbed n ∘ fun z : ℕ → X => fun i : Fin n => z i) (iidStreamLaw P) = _ rw [← Measure.map_map (measurable_fixedSizeEmbed n) (by fun_prop), iidStreamLaw_map_finPrefix]

lemma finiteMarkedPoissonSampleLaw_map_count (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : Measure.map FiniteSample.count (finiteMarkedPoissonSampleLaw P R lam) = poissonMeasure lam := by exact finitePoissonSampleLaw_map_count (P.prod R) lam

lemma finiteMeasureMarkedPoissonLaw_map_count (ν : Measure X) [IsFiniteMeasure ν] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : Measure.map FiniteSample.count (finiteMeasureMarkedPoissonLaw ν P₀ R lam) = poissonMeasure (lam * finiteMeasureMass ν) := by exact finiteMarkedPoissonSampleLaw_map_count (normalizedFiniteMeasure ν P₀) R (lam * finiteMeasureMass ν)

lemma klDiv_finiteMeasureMarkedPoissonLaw_le [StandardBorelSpace X] (ν₀ ν₁ : Measure X) [IsFiniteMeasure ν₀] [IsFiniteMeasure ν₁] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (B : ℝ≥0∞) (hmass : ν₀ univ = ν₁ univ) (hKL : klDiv ν₀ ν₁ ≤ B) : klDiv (finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam) (finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) ≤ (lam : ℝ≥0∞) * B := by rw [klDiv_finiteMeasureMarkedPoissonLaw ν₀ ν₁ P₀ R lam hmass] exact mul_le_mul_right hKL (lam : ℝ≥0∞)

-- @node: measurable_finiteSampleMap lemma measurable_finiteSampleMap {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (f : X → Y) (hf : Measurable f) : Measurable (finiteSampleMap f : FiniteSample X → FiniteSample Y) := by intro s hs rw [MeasurableSpace.measurableSet_iInf] at hs ⊢ intro n let g : (Fin n → X) → (Fin n → Y) := fun x i => f (x i) have hg : Measurable g := measurable_pi_lambda _ fun i => hf.comp (measurable_pi_apply i) have hsn := hs n change MeasurableSet (fixedSizeEmbed n ⁻¹' s) at hsn change MeasurableSet ((fun x : Fin n → X => ⟨n, fun i => f (x i)⟩) ⁻¹' s) exact hsn.preimage hg

-- @node: finiteSampleMap_fixedSizeEmbed lemma finiteSampleMap_fixedSizeEmbed {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (f : X → Y) (n : ℕ) (x : Fin n → X) : finiteSampleMap f (fixedSizeEmbed n x) = fixedSizeEmbed n (fun i => f (x i)) := rfl

-- @node: cellObservationLaw_eq_of_restrict_eq lemma cellObservationLaw_eq_of_restrict_eq {X ι : Type*} [MeasurableSpace X] [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (p : FiniteMeasurablePartition X ι) (μ ν : Measure X) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (j : ι) (hpos : μ (p.cellSet j) ≠ 0) (hmass : μ (p.cellSet j) = ν (p.cellSet j)) (hrest : μ.restrict (p.cellSet j) = ν.restrict (p.cellSet j)) : p.cellObservationLaw μ j = p.cellObservationLaw ν j := by unfold FiniteMeasurablePartition.cellObservationLaw have hν : ν (p.cellSet j) ≠ 0 := by simpa [← hmass] rw [dif_neg hpos, dif_neg hν, ← hmass, hrest]

-- @node: measurable_canonicalPrefixObservations lemma measurable_canonicalPrefixObservations {X : Type*} [MeasurableSpace X] (x₀ : X) (n : ℕ) : Measurable (canonicalPrefixObservations x₀ n : FiniteSample (X × ℝ) → Fin n → X) := by unfold canonicalPrefixObservations apply measurable_pi_lambda intro k t ht rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fun x : Fin m → X × ℝ => (if h : n ≤ m then fun k => (x (Fin.castLE h k)).1 else fun _ => x₀) k) ⁻¹' t) by_cases h : n ≤ m · simp only [dif_pos h] exact ht.preimage ((measurable_pi_apply (Fin.castLE h k)).fst) · simp only [dif_neg h] exact measurable_const ht

-- @node: map_canonicalPrefixObservations_restrict_count_ge lemma map_canonicalPrefixObservations_restrict_count_ge {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] [NullSingletonClass R] (lam : ℝ≥0) (x₀ : X) (n : ℕ) : Measure.map (canonicalPrefixObservations x₀ n) ((canonicalMarkedPoissonSampleLaw P R lam).restrict (FiniteSample.count ⁻¹' Ici n)) = (poissonMeasure lam) (Ici n) • Measure.pi (fun _ : Fin n => P) := by let μ := finiteMarkedPoissonSampleLaw P R lam have hcount : orderByMarks ⁻¹' (FiniteSample.count ⁻¹' Ici n : Set (FiniteSample (X × ℝ))) = FiniteSample.count ⁻¹' Ici n := by ext s change (n ≤ (orderByMarks s).count) ↔ n ≤ s.count rw [orderByMarks_count] rw [canonicalMarkedPoissonSampleLaw, Measure.restrict_map measurable_orderByMarks (measurable_finiteSample_count (measurableSet_Ici)), hcount, Measure.map_map (measurable_canonicalPrefixObservations x₀ n) measurable_orderByMarks] have hfun : canonicalPrefixObservations x₀ n ∘ orderByMarks = retainedObservations x₀ n := by funext s unfold canonicalPrefixObservations retainedObservations by_cases h : n ≤ s.count · simp only [orderByMarks_count, dif_pos h, Function.comp_apply] funext k congr 2 · simp only [orderByMarks_count, dif_neg h, Function.comp_apply] rw [hfun] exact map_retainedObservations_restrict_count_ge P R lam x₀ n

lemma poisson_two_n_lower_tail (n : ℕ) : (poissonMeasure (2 * n)) {k | k < n} ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) := by rw [show {k : ℕ | k < n} = (↑(range n) : Set ℕ) by ext k; simp] rw [← MeasureTheory.sum_measure_singleton] simp_rw [poissonMeasure_singleton_eq_poissonPMF] have hterm : ∀ k ∈ range n, poissonPMF (2 * n) k ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) * poissonPMF n k := by intro k hk have hreal : poissonPMFReal (2 * (n : ℝ≥0)) k ≤ exp (-(n : ℝ) * (1 - log 2)) * poissonPMFReal (n : ℝ≥0) k := by unfold poissonPMFReal rw [← mul_div_assoc] apply (div_le_div_iff_of_pos_right (by positivity : (0 : ℝ) < k.factorial)).2 have hn0 : (0 : ℝ) ≤ n := by positivity have hpow : (2 : ℝ) ^ k ≤ 2 ^ n := pow_le_pow_right₀ (by norm_num) (Finset.mem_range.1 hk).le have htarget : exp (-(n : ℝ) * (1 - log 2)) = exp (-(n : ℝ)) * (2 : ℝ) ^ n := by rw [show -(n : ℝ) * (1 - log 2) = -(n : ℝ) + log 2 * n by ring, Real.exp_add, show log 2 * (n : ℝ) = (n : ℝ) * log 2 by ring, Real.exp_nat_mul, Real.exp_log (by norm_num : (0 : ℝ) < 2)] have hexp2 : exp (-((2 : ℝ) * (n : ℝ))) = exp (-(n : ℝ)) * exp (-(n : ℝ)) := by rw [← Real.exp_add] congr 1 ring norm_num only [NNReal.smul_def, NNReal.coe_natCast, NNReal.coe_mul, Nat.cast_ofNat] rw [mul_pow, htarget] change exp (-(2 * (n : ℝ))) * ((2 : ℝ) ^ k * (n : ℝ) ^ k) ≤ _ rw [hexp2] calc exp (-(n : ℝ)) * exp (-(n : ℝ)) * ((2 : ℝ) ^ k * (n : ℝ) ^ k) = (exp (-(n : ℝ)) * exp (-(n : ℝ)) * (n : ℝ) ^ k) * 2 ^ k := by ring _ ≤ (exp (-(n : ℝ)) * exp (-(n : ℝ)) * (n : ℝ) ^ k) * 2 ^ n := mul_le_mul_of_nonneg_left hpow (by positivity) _ = exp (-(n : ℝ)) * 2 ^ n * (exp (-(n : ℝ)) * (n : ℝ) ^ k) := by ring unfold poissonPMF change ofReal (poissonPMFReal (2 * n) k) ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) * ofReal (poissonPMFReal n k) rw [← ENNReal.ofReal_mul (Real.exp_pos _).le] exact ENNReal.ofReal_le_ofReal hreal calc ∑ k ∈ range n, poissonPMF (2 * n) k ≤ ∑ k ∈ range n, ofReal (exp (-(n : ℝ) * (1 - log 2))) * poissonPMF n k := Finset.sum_le_sum hterm _ = ofReal (exp (-(n : ℝ) * (1 - log 2))) * ∑ k ∈ range n, poissonPMF n k := by rw [Finset.mul_sum] _ ≤ ofReal (exp (-(n : ℝ) * (1 - log 2))) * 1 := by gcongr exact ((poissonPMF n).property.summable.sum_le_tsum _ (fun _ _ => bot_le)).trans_eq (poissonPMF n).property.tsum_eq _ = _ := mul_one _

lemma finiteSamplePaddedStream_measurable {X : Type*} [MeasurableSpace X] (x0 : X) : Measurable (finiteSamplePaddedStream x0) := by intro t ht rw [MeasurableSpace.measurableSet_iInf] intro n change MeasurableSet ((fun s : Fin n → X => finiteSamplePaddedStream x0 ⟨n, s⟩) ⁻¹' t) apply ht.preimage apply measurable_const.prodMk apply measurable_pi_lambda intro k by_cases hk : k < n · let i : Fin n := ⟨k, hk⟩ simpa [finiteSamplePaddedStream, FiniteSample.count, FiniteSample.points, hk, i] using (measurable_pi_apply i : Measurable (fun s : Fin n → X => s i)) · simp [finiteSamplePaddedStream, FiniteSample.count, hk]

lemma streamToFiniteSample_paddedStream {X : Type*} [MeasurableSpace X] (x0 : X) (s : FiniteSample X) : streamToFiniteSample (finiteSamplePaddedStream x0 s) = s := by cases s with | mk n s => change (⟨n, fun k => if h : k < n then s ⟨k, h⟩ else x0⟩ : Σ n : ℕ, Fin n → X) = ⟨n, s⟩ congr funext k simp

lemma finiteSamplePaddedStream_range {X : Type*} [MeasurableSpace X] (x0 : X) : range (finiteSamplePaddedStream x0) = {z : ℕ × (ℕ → X) | ∀ k, z.1 ≤ k → z.2 k = x0} := by ext z constructor · rintro ⟨s, rfl⟩ k hk have hnot : ¬k < s.count := Nat.not_lt_of_ge hk simp [finiteSamplePaddedStream, hnot] · intro hz refine ⟨streamToFiniteSample z, ?_⟩ apply Prod.ext · rfl · funext k by_cases hk : k < z.1 · simp [finiteSamplePaddedStream, FiniteSample.count, FiniteSample.points, streamToFiniteSample, hk] · simp [finiteSamplePaddedStream, FiniteSample.count, FiniteSample.points, streamToFiniteSample, hk, hz k (Nat.le_of_not_gt hk)]

lemma canonicalMarkedPoissonSampleLaw_map_count {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : Measure.map FiniteSample.count (canonicalMarkedPoissonSampleLaw P R lam) = poissonMeasure lam := by unfold canonicalMarkedPoissonSampleLaw rw [Measure.map_map measurable_finiteSample_count measurable_orderByMarks] simpa only [Function.comp_def, orderByMarks_count] using finiteMarkedPoissonSampleLaw_map_count P R lam

theorem finiteMeasureMarkedPoissonLaw_probability_eq {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (P0 : Measure X) [IsProbabilityMeasure P0] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) : finiteMeasureMarkedPoissonLaw P P0 R lam = finiteMarkedPoissonSampleLaw P R lam := by have hP : P ≠ 0 := by intro h have : P univ = 1 := by simp simp [h] at this have hnorm : normalizedFiniteMeasure P P0 = P := by unfold normalizedFiniteMeasure rw [dif_neg hP] simp have hmass : finiteMeasureMass P = 1 := by unfold finiteMeasureMass simp unfold finiteMeasureMarkedPoissonLaw rw [hmass, mul_one] congr 2

lemma poissonIIDStreamLaw_map_count (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) : Measure.map fst (poissonIIDStreamLaw P lam) = poissonMeasure lam := by unfold poissonIIDStreamLaw iidStreamLaw rw [Measure.map_fst_prod, measure_univ, one_smul]

lemma poissonIIDStreamLaw_map_finPrefix (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (n : ℕ) : Measure.map (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) (poissonIIDStreamLaw P lam) = Measure.pi (fun _ : Fin n => P) := by rw [show (fun z : ℕ × (ℕ → X) => fun i : Fin n => z.2 i) = (fun z : ℕ → X => fun i : Fin n => z i) ∘ snd by rfl, ← Measure.map_map (by fun_prop) (by fun_prop)] unfold poissonIIDStreamLaw rw [Measure.map_snd_prod, measure_univ, one_smul, iidStreamLaw_map_finPrefix]