Stat.Minimax.Moment­Matched­Mixture.Finite­Signed­Moment­Marked­Poisson­Mixture

theorem variation_eq_absoluteMeasure (C : NormalizedFiniteSignedMomentCertificate ι L) : C.signedMeasure.variation = C.absoluteMeasure := by rw [signedMeasure_eq_absoluteMeasure_withDensity, Measure.variation_withDensityᵥ (integrable_atomicPolarSign_absoluteMeasure C)] calc C.absoluteMeasure.withDensity (fun x => ‖atomicPolarSign C x‖ₑ) = C.absoluteMeasure.withDensity 1 := by apply withDensity_congr_ae filter_upwards [abs_atomicPolarSign_ae_absoluteMeasure C] with x hx rw [← ofReal_norm, Real.norm_eq_abs, hx] simp _ = C.absoluteMeasure := withDensity_one

theorem signedMeasure_univ_eq_zero (C : NormalizedFiniteSignedMomentCertificate ι L) : C.signedMeasure univ = 0 := by rw [signedMeasure] rw [finsetSum_signedMeasure_apply] simpa using C.moments_zero 0 (zero_le L)

theorem integral_pow_signedMeasure_eq_zero (C : NormalizedFiniteSignedMomentCertificate ι L) (j : ℕ) (hj : j ≤ L) : ∫ᵛ x, x ^ j ∂<•C.signedMeasure = 0 := by rw [signedMeasure] rw [VectorMeasure.integral_finsetSum_vectorMeasure (fun i _ => by change Integrable (fun x : ℝ => x ^ j) (VectorMeasure.dirac (C.node i) (C.weight i)).variation rw [VectorMeasure.variation_dirac] exact (integrable_dirac (by simp)).smul_measure (by simp))] simpa using C.moments_zero j hj

theorem abs_polarSign_ae (C : NormalizedFiniteSignedMomentCertificate ι L) : ∀ᵐ x ∂C.signedMeasure.variation, |C.polarSign x| = 1 := by rw [variation_eq_absoluteMeasure] exact abs_atomicPolarSign_ae_absoluteMeasure C

theorem integrable_polarSign (C : NormalizedFiniteSignedMomentCertificate ι L) : Integrable C.polarSign C.signedMeasure.variation := by rw [variation_eq_absoluteMeasure] exact integrable_atomicPolarSign_absoluteMeasure C

theorem signedMeasure_eq_withDensity_polarSign (C : NormalizedFiniteSignedMomentCertificate ι L) : C.signedMeasure = C.signedMeasure.variation.withDensityᵥ C.polarSign := by rw [variation_eq_absoluteMeasure] exact signedMeasure_eq_absoluteMeasure_withDensity C

theorem jordanDecomposition_posPart_eq (C : NormalizedFiniteSignedMomentCertificate ι L) : C.signedMeasure.toJordanDecomposition.posPart = (2 : ℝ≥0∞)⁻¹ • C.positivePrior := by have hJ := SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity (s := C.signedMeasure) (t := 0) (μ := C.absoluteMeasure) (measurable_atomicPolarSign C) (integrable_atomicPolarSign_absoluteMeasure C) VectorMeasure.MutuallySingular.zero_left (by simpa using signedMeasure_eq_absoluteMeasure_withDensity C) have hpos := congrArg JordanDecomposition.posPart hJ calc C.signedMeasure.toJordanDecomposition.posPart = C.absoluteMeasure.withDensity (fun x => ofReal (atomicPolarSign C x)) := by simpa [SignedMeasure.toJordanDecomposition_zero, JordanDecomposition.zero_posPart] using hpos _ = ∑ i, ofReal (max (C.weight i) 0) • Measure.dirac (C.node i) := absoluteMeasure_withDensity_pos C _ = (2 : ℝ≥0∞)⁻¹ • C.positivePrior := (half_positivePrior C).symm

theorem jordanDecomposition_negPart_eq (C : NormalizedFiniteSignedMomentCertificate ι L) : C.signedMeasure.toJordanDecomposition.negPart = (2 : ℝ≥0∞)⁻¹ • C.negativePrior := by have hJ := SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity (s := C.signedMeasure) (t := 0) (μ := C.absoluteMeasure) (measurable_atomicPolarSign C) (integrable_atomicPolarSign_absoluteMeasure C) VectorMeasure.MutuallySingular.zero_left (by simpa using signedMeasure_eq_absoluteMeasure_withDensity C) have hneg := congrArg JordanDecomposition.negPart hJ calc C.signedMeasure.toJordanDecomposition.negPart = C.absoluteMeasure.withDensity (fun x => ofReal (-atomicPolarSign C x)) := by simpa [SignedMeasure.toJordanDecomposition_zero, JordanDecomposition.zero_negPart] using hneg _ = ∑ i, ofReal (max (-C.weight i) 0) • Measure.dirac (C.node i) := absoluteMeasure_withDensity_neg C _ = (2 : ℝ≥0∞)⁻¹ • C.negativePrior := (half_negativePrior C).symm

theorem jordanPriors_moments_eq (C : NormalizedFiniteSignedMomentCertificate ι L) (j : ℕ) (hj : j ≤ L) : ∫ x, x ^ j ∂C.positivePrior = ∫ x, x ^ j ∂C.negativePrior := by have h := prior_integral_sub C (fun x => x ^ j) rw [C.moments_zero j hj, mul_zero] at h linarith

theorem jordanPriors_ae_mem_range (C : NormalizedFiniteSignedMomentCertificate ι L) : (∀ᵐ x ∂C.positivePrior, x ∈ range C.node) ∧ ∀ᵐ x ∂C.negativePrior, x ∈ range C.node := by classical constructor · rw [positivePrior, ae_finsetSum_measure_iff] intro i hi apply Measure.ae_smul_measure exact (ae_dirac_iff (Set.finite_range C.node).measurableSet).2 ⟨i, rfl⟩ · rw [negativePrior, ae_finsetSum_measure_iff] intro i hi apply Measure.ae_smul_measure exact (ae_dirac_iff (Set.finite_range C.node).measurableSet).2 ⟨i, rfl⟩

theorem orientedPriors_moments_eq (C : NormalizedFiniteSignedMomentCertificate ι L) (f : ℝ → ℝ) (j : ℕ) (hj : j ≤ L) : ∫ x, x ^ j ∂C.orientedPrior0 f = ∫ x, x ^ j ∂C.orientedPrior1 f := by by_cases h : 0 ≤ ∑ i, C.weight i * f (C.node i) · rw [orientedPrior0, if_pos h, orientedPrior1, if_pos h] exact (jordanPriors_moments_eq C j hj).symm · rw [orientedPrior0, if_neg h, orientedPrior1, if_neg h] exact jordanPriors_moments_eq C j hj

theorem aggregatePoissonKernel_apply (ε a t p : ℝ) : aggregatePoissonKernel ε a t p = aggregatePoissonLaw ε a t p := by unfold aggregatePoissonKernel aggregatePoissonLaw rw [Kernel.prod_apply, aggregatePoissonKernelOfRealRate_apply _ (by change Measurable (fun p : ℝ => t * ε * (p + a)) fun_prop), aggregatePoissonKernelOfRealRate_apply _ (by change Measurable (fun p : ℝ => t * ((1 - ε) * p - ε * a)) fun_prop)]

theorem exists_geometric_sqrt_exponentialSeriesTail_bound (A : ℝ) (hA : 0 < A) : ∃ b D ρ : ℝ, 0 < b ∧ 0 < D ∧ ρ ∈ Ioo (0 : ℝ) 1 ∧ ∀ (L : ℕ) (x : ℝ), 0 ≤ x → x ≤ b * L → sqrt (exponentialSeriesTail L (A * x)) ≤ D * ρ ^ L := by refine ⟨1 / (16 * A * exp 1), 1, 1 / 2, by positivity, by norm_num, ⟨by norm_num, by norm_num⟩, ?_⟩ intro L x hx hband obtain rfl | hL := L.eq_zero_or_pos · have hxle : x ≤ 0 := by simpa using hband have hxeq : x = 0 := le_antisymm hxle hx subst x have htailzero : exponentialSeriesTail 0 0 = 0 := by unfold exponentialSeriesTail rw [show (fun n : ℕ => if 0 < n then (0 : ℝ) ^ n / (n.factorial : ℝ) else 0) = 0 by funext n split_ifs with hn · simp [zero_pow (Nat.ne_of_gt hn)] · rfl] exact tsum_zero simp only [mul_zero] rw [htailzero, Real.sqrt_zero, pow_zero] norm_num have hz : 0 ≤ A * x := mul_nonneg hA.le hx have hzL : A * x ≤ (L : ℝ) / (16 * exp 1) := by calc A * x ≤ A * ((1 / (16 * A * exp 1)) * (L : ℝ)) := mul_le_mul_of_nonneg_left hband hA.le _ = (L : ℝ) / (16 * exp 1) := by field_simp let f : ℕ → ℝ := fun n => if L < n then (A * x) ^ n / (n.factorial : ℝ) else 0 let g : ℕ → ℝ := fun n => if L < n then (1 / 4 : ℝ) ^ n else 0 have hq : Summable (fun n : ℕ => (1 / 4 : ℝ) ^ n) := summable_geometric_of_norm_lt_one (by norm_num) have hg : Summable g := by apply hq.of_nonneg_of_le · intro n dsimp [g] positivity · intro n dsimp [g] split_ifs · rfl · positivity have hf_nonneg : ∀ n, 0 ≤ f n := by intro n dsimp [f] positivity have hfg : ∀ n, f n ≤ g n := by intro n dsimp [f, g] split_ifs with hn · exact exponential_term_le_quarter_pow L n (A * x) hz hzL hn · rfl have hf : Summable f := hg.of_nonneg_of_le hf_nonneg hfg have htail : exponentialSeriesTail L (A * x) ≤ (1 / 4 : ℝ) ^ L := by unfold exponentialSeriesTail change (∑' n, f n) ≤ _ exact (hf.tsum_le_tsum hfg hg).trans (geometric_quarter_tail L) rw [one_mul, Real.sqrt_le_iff] refine ⟨by positivity, htail.trans_eq ?_⟩ rw [show (1 / 4 : ℝ) = (1 / 2) ^ 2 by norm_num, ← pow_mul, ← pow_mul] congr 1 omega

theorem exists_aggregatePoisson_jordan_sqrt_tail_bound (ε κ : ℝ) (hε : 0 < ε) (hεhalf : ε < 1 / 2) (hκ : κ = (1 - 2 * ε) / ε) : ∃ A : ℝ, 0 < A ∧ ∀ {ι : Type*} [Fintype ι] {L : ℕ} (C : NormalizedFiniteSignedMomentCertificate ι L) (a B t : ℝ), 0 < a → 0 < B → 0 < t → (∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) → tvDist (aggregatePoissonPredictive C.positivePrior ε a t) (aggregatePoissonPredictive C.negativePrior ε a t) ≤ sqrt (exponentialSeriesTail L (A * (t * B))) := by have hden : 0 < 1 - 2 * ε := by nlinarith have hκpos : 0 < κ := by rw [hκ]; positivity let A : ℝ := 2 * ε + 2 * (1 - ε) ^ 2 / ε have hA : 0 < A := by dsimp [A] positivity refine ⟨A, hA, ?_⟩ intro ι _ L C a B t ha hB ht hsupp let l : ℝ := a / κ let c : ℝ := (l + B) / 2 let R : ℝ := (B - l) / 2 let qT : ℝ := t * ε * (c + a) let qC : ℝ := t * ((1 - ε) * c - ε * a) let sT : ℝ := t * ε let sC : ℝ := t * (1 - ε) let lambda : ℝ := sT ^ 2 / qT + sC ^ 2 / qC let πP : Measure ℝ := Measure.map (fun p : ℝ => p - c) C.positivePrior let πN : Measure ℝ := Measure.map (fun p : ℝ => p - c) C.negativePrior let Kc : Kernel ℝ AggregatePoissonObservation := (aggregatePoissonKernel ε a t).comap (fun θ : ℝ => θ + c) (by fun_prop) let Q : Measure AggregatePoissonObservation := (poissonMeasure (toNNReal qT)).prod (poissonMeasure (toNNReal qC)) let likelihood : ℝ → AggregatePoissonObservation → ℝ := aggregateCenteredLikelihood qT qC sT sC have hlB : l ≤ B := by rcases hsupp.exists with ⟨p, hp⟩ exact hp.1.trans hp.2 have hlpos : 0 < l := div_pos ha hκpos have ha_le : a ≤ κ * B := by simpa [mul_comm] using (div_le_iff₀ hκpos).mp (by simpa [l] using hlB) have hcontrol_l : 0 < (1 - ε) * l - ε * a := by have hinv : κ⁻¹ = ε / (1 - 2 * ε) := by rw [hκ, inv_div] have hden' : 1 - ε * 2 ≠ 0 := by nlinarith have hid : (1 - ε) * l - ε * a = a * ε ^ 2 / (1 - 2 * ε) := by dsimp [l] rw [div_eq_mul_inv, hinv] field_simp [hden'] ring rw [hid] positivity have hcontrol_B : ε * B ≤ (1 - ε) * B - ε * a := by have hκmul : ε * κ = 1 - 2 * ε := by rw [hκ] field_simp nlinarith [mul_le_mul_of_nonneg_left ha_le hε.le] have hc_ge_halfB : B / 2 ≤ c := by dsimp [c] nlinarith [hlpos.le] have hRnonneg : 0 ≤ R := by dsimp [R]; linarith have hRleB : R ≤ B := by dsimp [R]; nlinarith [hlpos.le] have hqT_lower : t * ε * (B / 2) ≤ qT := by dsimp [qT] apply mul_le_mul_of_nonneg_left _ (mul_nonneg ht.le hε.le) linarith [ha] have hqT : 0 < qT := lt_of_lt_of_le (by positivity) hqT_lower have hqC_lower : t * (ε * B / 2) ≤ qC := by dsimp [qC, c] have hcidentity : (1 - ε) * ((l + B) / 2) - ε * a = (((1 - ε) * l - ε * a) + ((1 - ε) * B - ε * a)) / 2 := by ring rw [hcidentity] have : ε * B / 2 ≤ (((1 - ε) * l - ε * a) + ((1 - ε) * B - ε * a)) / 2 := by nlinarith [hcontrol_l, hcontrol_B] exact mul_le_mul_of_nonneg_left this ht.le have hqC : 0 < qC := lt_of_lt_of_le (by positivity) hqC_lower have hlambda : 0 ≤ lambda := by dsimp [lambda] positivity have hcenter_mem (θ : ℝ) (hθ : |θ| ≤ R) : θ + c ∈ Icc l B := by rw [abs_le] at hθ constructor <;> dsimp [c, R] at * <;> linarith have hrates (θ : ℝ) (hθ : |θ| ≤ R) : 0 ≤ qT + sT * θ ∧ 0 ≤ qC + sC * θ := by have hp := hcenter_mem θ hθ constructor · have : 0 < θ + c + a := lt_of_lt_of_le (add_pos hlpos ha) (by linarith [hp.1]) dsimp [qT, sT] nlinarith [mul_pos (mul_pos ht hε) this] · have hc0 : 0 ≤ (1 - ε) * (θ + c) - ε * a := (le_of_lt hcontrol_l).trans (by have he1 : 0 ≤ 1 - ε := by nlinarith nlinarith [mul_le_mul_of_nonneg_left hp.1 he1]) dsimp [qC, sC] nlinarith [mul_nonneg ht.le hc0] have hparamT (θ : ℝ) : aggregateTreatedRate ε a t (θ + c) = qT + sT * θ := by dsimp [aggregateTreatedRate, qT, sT] ring have hparamC (θ : ℝ) : aggregateControlRate ε a t (θ + c) = qC + sC * θ := by dsimp [aggregateControlRate, qC, sC] ring haveI : IsProbabilityMeasure πP := by dsimp [πP] exact Measure.isProbabilityMeasure_map (by fun_prop) haveI : IsProbabilityMeasure πN := by dsimp [πN] exact Measure.isProbabilityMeasure_map (by fun_prop) haveI : IsProbabilityMeasure Q := by dsimp [Q] infer_instance have hKprob : ∀ θ, IsProbabilityMeasure (Kc θ) := by intro θ dsimp [Kc] rw [aggregatePoissonKernel_apply] infer_instance have hmeas : Measurable (fun z : ℝ × AggregatePoissonObservation => likelihood z.1 z.2) := by exact measurable_aggregateCenteredLikelihood qT qC sT sC have hnonneg : ∀ θ, |θ| ≤ R → ∀ z, 0 ≤ likelihood θ z := by intro θ hθ z exact aggregateCenteredLikelihood_nonnegative qT qC sT sC θ hqT hqC (hrates θ hθ).1 (hrates θ hθ).2 z have hdensity : ∀ θ, |θ| ≤ R → Kc θ = Q.withDensity fun z => ofReal (likelihood θ z) := by intro θ hθ dsimp [Kc, Q, likelihood] rw [aggregatePoissonKernel_apply] exact aggregatePoissonLaw_centered_eq_withDensity ε a t c θ qT qC sT sC hqT hqC (hrates θ hθ).1 (hrates θ hθ).2 (hparamT θ) (hparamC θ) have hinner : ∀ θ, |θ| ≤ R → ∀ θ', |θ'| ≤ R → ∫ z, likelihood θ z * likelihood θ' z ∂Q = exp (lambda * θ * θ') := by intro θ hθ θ' hθ' exact aggregateCenteredLikelihood_inner qT qC sT sC θ θ' hqT hqC rcases jordanPriors_ae_of_variation C hsupp with ⟨hsuppP, hsuppN⟩ have hsuppπP : πP {θ | |θ| ≤ R} = 1 := by exact centered_map_supported C.positivePrior l B c R rfl rfl hsuppP have hsuppπN : πN {θ | |θ| ≤ R} = 1 := by exact centered_map_supported C.negativePrior l B c R rfl rfl hsuppN have hmom : ∀ n ≤ L, ∫ θ, θ ^ n ∂πP = ∫ θ, θ ^ n ∂πN := by intro n hn exact centered_map_moments_eq C l B c hsupp n hn have hlambdaR : lambda * R ^ 2 ≤ A * (t * B) := by have hqTbound : sT ^ 2 / qT ≤ 2 * t * ε / B := by rw [div_le_iff₀ hqT] have := hqT_lower dsimp [sT] field_simp nlinarith have hqCbound : sC ^ 2 / qC ≤ 2 * t * (1 - ε) ^ 2 / (ε * B) := by rw [div_le_iff₀ hqC] have := hqC_lower dsimp [sC] field_simp nlinarith [sq_nonneg (1 - ε)] have hR2 : R ^ 2 ≤ B ^ 2 := by nlinarith [sq_nonneg R, sq_nonneg B] dsimp [lambda, A] calc (sT ^ 2 / qT + sC ^ 2 / qC) * R ^ 2 ≤ (2 * t * ε / B + 2 * t * (1 - ε) ^ 2 / (ε * B)) * R ^ 2 := by gcongr _ ≤ (2 * t * ε / B + 2 * t * (1 - ε) ^ 2 / (ε * B)) * B ^ 2 := by gcongr _ = (2 * ε + 2 * (1 - ε) ^ 2 / ε) * (t * B) := by field_simp have htv := momentMatchedMixture_tv_le_sqrt_tail_of_supported πP πN Kc Q likelihood hKprob lambda R L hlambda hRnonneg hmeas hnonneg hdensity hinner hsuppπP hsuppπN hmom rw [priorPredictive_centered_map C.positivePrior (aggregatePoissonKernel ε a t) c, priorPredictive_centered_map C.negativePrior (aggregatePoissonKernel ε a t) c] at htv exact htv.trans (Real.sqrt_le_sqrt (exponentialSeriesTail_mono L (mul_nonneg hlambda (sq_nonneg R)) hlambdaR))

theorem markedPoissonKernel_apply (ε a u v : ℝ) (h : ℝ → ℝ) (hh : Measurable h) (branch : Bool) (p : ℝ) : markedPoissonKernel ε a u v h hh branch p = markedPoissonLaw ε a u v h branch p := by unfold markedPoissonKernel markedPoissonLaw rw [Kernel.prod_apply, Kernel.prod_apply, Kernel.prod_apply] rw [poissonKernelOfRealRate_apply _ (by cases branch <;> simp [treatedMass, branchMark] <;> fun_prop), poissonKernelOfRealRate_apply _ (by cases branch <;> simp [treatedMass, branchMark] <;> fun_prop), poissonKernelOfRealRate_apply _ (by simp [treatedMass] <;> fun_prop), poissonKernelOfRealRate_apply _ (by simp [controlMass, treatedMass] <;> fun_prop)]

theorem markedPoissonPredictive_isProbabilityMeasure {ι : Type*} [Fintype ι] {L : ℕ} (C : NormalizedFiniteSignedMomentCertificate ι L) (ε a u v κ B : ℝ) (branch : Bool) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : IsProbabilityMeasure (C.markedPoissonPredictive ε a u v branch) := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := C.zeroInflatedPrior_isProbabilityMeasure a κ B ha hκ hsupp exact priorPredictive_isProbability (C.zeroInflatedPrior a) (markedPoissonKernel ε a u v C.polarSign C.measurable_polarSign branch) (fun p => by rw [markedPoissonKernel_apply] infer_instance)

theorem restrict_markedPoissonPredictive_noLabeledTreated_eq {ι : Type*} [Fintype ι] {L : ℕ} (C : NormalizedFiniteSignedMomentCertificate ι L) (ε a u v κ B : ℝ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : (C.markedPoissonPredictive ε a u v false).restrict noLabeledTreated = (C.markedPoissonPredictive ε a u v true).restrict noLabeledTreated := by apply Measure.ext_of_singleton intro z rw [Measure.restrict_apply (measurableSet_singleton z), Measure.restrict_apply (measurableSet_singleton z)] by_cases hz : z ∈ noLabeledTreated · have hinter : {z} ∩ noLabeledTreated = {z} := Set.inter_eq_left.mpr (Set.singleton_subset_iff.mpr hz) rw [hinter] unfold markedPoissonPredictive rw [priorPredictive_apply _ _ (measurableSet_singleton z), priorPredictive_apply _ _ (measurableSet_singleton z)] apply lintegral_congr intro p rw [markedPoissonKernel_apply, markedPoissonKernel_apply] exact markedPoissonLaw_singleton_eq_of_noLabeledTreated ε a u v C.polarSign p z hz · have hinter : {z} ∩ noLabeledTreated = ∅ := Set.disjoint_iff_inter_eq_empty.mp (Set.disjoint_singleton_left.mpr hz) rw [hinter] simp

theorem tvDist_markedPoissonPredictive_le_palm_aggregate {ι : Type*} [Fintype ι] {L : ℕ} (C : NormalizedFiniteSignedMomentCertificate ι L) (ε κ a B u v : ℝ) (hε : 0 < ε) (hεhalf : ε < 1 / 2) (hκ : κ = (1 - 2 * ε) / ε) (ha : 0 < a) (hB : 0 < B) (hu : 0 ≤ u) (hv : 0 ≤ v) (ht : 0 < u + v) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : tvDist (C.markedPoissonPredictive ε a u v false) (C.markedPoissonPredictive ε a u v true) ≤ u * ε * a * tvDist (aggregatePoissonPredictive C.positivePrior ε a (u + v)) (aggregatePoissonPredictive C.negativePrior ε a (u + v)) := by have hκpos : 0 < κ := by rw [hκ] apply div_pos · nlinarith · exact hε let q : unitInterval := ⟨u / (u + v), by constructor · positivity · rw [div_le_one ht] linarith⟩ let P := aggregatePoissonPredictive C.positivePrior ε a (u + v) let N := aggregatePoissonPredictive C.negativePrior ε a (u + v) let Kf := palmSplitKernel q true let Ks := palmSplitKernel q false let Mf := C.markedPoissonPredictive ε a u v false let Mt := C.markedPoissonPredictive ε a u v true let d : ℝ≥0∞ := ofReal (u * ε * a / 2) let _ : IsProbabilityMeasure P := priorPredictive_isProbability C.positivePrior (aggregatePoissonKernel ε a (u + v)) (fun p => by rw [aggregatePoissonKernel_apply]; infer_instance) let _ : IsProbabilityMeasure N := priorPredictive_isProbability C.negativePrior (aggregatePoissonKernel ε a (u + v)) (fun p => by rw [aggregatePoissonKernel_apply]; infer_instance) let _ : IsProbabilityMeasure Mf := C.markedPoissonPredictive_isProbabilityMeasure ε a u v κ B false ha hκpos hsupp let _ : IsProbabilityMeasure Mt := C.markedPoissonPredictive_isProbabilityMeasure ε a u v κ B true ha hκpos hsupp have hc : 0 ≤ u * ε * a := by positivity have hd : d.toReal = u * ε * a / 2 := by change (ofReal (u * ε * a / 2)).toReal = _ rw [ENNReal.toReal_ofReal] positivity let _ : IsFiniteMeasure (d • ((Kf ∘ₘ P) + (Ks ∘ₘ N))) := Measure.smul_finite _ (by simp [d]) let _ : IsFiniteMeasure (d • ((Kf ∘ₘ N) + (Ks ∘ₘ P))) := Measure.smul_finite _ (by simp [d]) let _ : IsFiniteMeasure (Mf + d • ((Kf ∘ₘ P) + (Ks ∘ₘ N))) := by infer_instance let _ : IsFiniteMeasure (Mt + d • ((Kf ∘ₘ N) + (Ks ∘ₘ P))) := by infer_instance have hbalance : Mf + d • ((Kf ∘ₘ P) + (Ks ∘ₘ N)) = Mt + d • ((Kf ∘ₘ N) + (Ks ∘ₘ P)) := by apply Measure.ext_of_measureReal_singleton rintro ⟨⟨x, y⟩, ⟨s, t⟩⟩ rw [measureReal_add_ennreal_smul_add Mf (Kf ∘ₘ P) (Ks ∘ₘ N) d (by simp [d]), measureReal_add_ennreal_smul_add Mt (Kf ∘ₘ N) (Ks ∘ₘ P) d (by simp [d])] rcases x with _ | k · rcases y with _ | l · have hm : Mf.real {((0, 0), (s, t))} = Mt.real {((0, 0), (s, t))} := by have hr := congrArg (fun μ : Measure MarkedPoissonObservation => μ.real {((0, 0), (s, t))}) (C.restrict_markedPoissonPredictive_noLabeledTreated_eq ε a u v κ B ha hκpos hsupp) simpa [Mf, Mt, Measure.restrict_apply, noLabeledTreated] using hr have hp := palmSplit_bind_no_labeled_eq q P s t have hn := palmSplit_bind_no_labeled_eq q N s t change Mf.real {((0, 0), (s, t))} + d.toReal * ((Kf ∘ₘ P).real {((0, 0), (s, t))} + (Ks ∘ₘ N).real {((0, 0), (s, t))}) = Mt.real {((0, 0), (s, t))} + d.toReal * ((Kf ∘ₘ N).real {((0, 0), (s, t))} + (Ks ∘ₘ P).real {((0, 0), (s, t))}) change (palmSplitKernel q false ∘ₘ P).real {((0, 0), (s, t))} = (palmSplitKernel q true ∘ₘ P).real {((0, 0), (s, t))} at hp change (palmSplitKernel q false ∘ₘ N).real {((0, 0), (s, t))} = (palmSplitKernel q true ∘ₘ N).real {((0, 0), (s, t))} at hn rw [hm, ← hp, ← hn] ring · have hm := markedPredictive_real_target_sub C ε κ a B u v hε hεhalf hκ ha hu hv ht hsupp false l s t have hPf := palmSplit_bind_wrong_target q false P l s t have hNf := palmSplit_bind_wrong_target q false N l s t change Mf.real {palmSplitTarget false l s t} + d.toReal * ((Kf ∘ₘ P).real {palmSplitTarget false l s t} + (Ks ∘ₘ N).real {palmSplitTarget false l s t}) = Mt.real {palmSplitTarget false l s t} + d.toReal * ((Kf ∘ₘ N).real {palmSplitTarget false l s t} + (Ks ∘ₘ P).real {palmSplitTarget false l s t}) change Mf.real {palmSplitTarget false l s t} - Mt.real {palmSplitTarget false l s t} = _ at hm have hm' : Mf.real {palmSplitTarget false l s t} - Mt.real {palmSplitTarget false l s t} = (u * ε * a / 2) * ((Ks ∘ₘ P).real {palmSplitTarget false l s t} - (Ks ∘ₘ N).real {palmSplitTarget false l s t}) := by simpa [q, P, N, Ks, Mf, Mt] using hm change (Kf ∘ₘ P).real {palmSplitTarget false l s t} = 0 at hPf change (Kf ∘ₘ N).real {palmSplitTarget false l s t} = 0 at hNf rw [hPf, hNf, hd] nlinarith [hm'] · rcases y with _ | l · have hm := markedPredictive_real_target_sub C ε κ a B u v hε hεhalf hκ ha hu hv ht hsupp true k s t have hPs := palmSplit_bind_wrong_target q true P k s t have hNs := palmSplit_bind_wrong_target q true N k s t change Mf.real {palmSplitTarget true k s t} + d.toReal * ((Kf ∘ₘ P).real {palmSplitTarget true k s t} + (Ks ∘ₘ N).real {palmSplitTarget true k s t}) = Mt.real {palmSplitTarget true k s t} + d.toReal * ((Kf ∘ₘ N).real {palmSplitTarget true k s t} + (Ks ∘ₘ P).real {palmSplitTarget true k s t}) change Mf.real {palmSplitTarget true k s t} - Mt.real {palmSplitTarget true k s t} = _ at hm have hm' : Mf.real {palmSplitTarget true k s t} - Mt.real {palmSplitTarget true k s t} = -(u * ε * a / 2) * ((Kf ∘ₘ P).real {palmSplitTarget true k s t} - (Kf ∘ₘ N).real {palmSplitTarget true k s t}) := by simpa [q, P, N, Kf, Mf, Mt] using hm change (Ks ∘ₘ P).real {palmSplitTarget true k s t} = 0 at hPs change (Ks ∘ₘ N).real {palmSplitTarget true k s t} = 0 at hNs rw [hPs, hNs, hd] nlinarith [hm'] · have hm := markedPredictive_real_both_positive_sub_eq_zero C ε a u v κ B ha hκpos hsupp k l s t have hPf := palmSplit_bind_both_positive q true P k l s t have hNf := palmSplit_bind_both_positive q true N k l s t have hPs := palmSplit_bind_both_positive q false P k l s t have hNs := palmSplit_bind_both_positive q false N k l s t change Mf.real {((k + 1, l + 1), (s, t))} + d.toReal * ((Kf ∘ₘ P).real {((k + 1, l + 1), (s, t))} + (Ks ∘ₘ N).real {((k + 1, l + 1), (s, t))}) = Mt.real {((k + 1, l + 1), (s, t))} + d.toReal * ((Kf ∘ₘ N).real {((k + 1, l + 1), (s, t))} + (Ks ∘ₘ P).real {((k + 1, l + 1), (s, t))}) change Mf.real {((k + 1, l + 1), (s, t))} - Mt.real {((k + 1, l + 1), (s, t))} = 0 at hm change (Kf ∘ₘ P).real {((k + 1, l + 1), (s, t))} = 0 at hPf change (Kf ∘ₘ N).real {((k + 1, l + 1), (s, t))} = 0 at hNf change (Ks ∘ₘ P).real {((k + 1, l + 1), (s, t))} = 0 at hPs change (Ks ∘ₘ N).real {((k + 1, l + 1), (s, t))} = 0 at hNs rw [hPf, hNf, hPs, hNs] linarith change tvDist Mf Mt ≤ u * ε * a * tvDist P N unfold tvDist apply ciSup_le rintro ⟨A, hA⟩ have hb := congrArg (fun μ : Measure MarkedPoissonObservation => μ.real A) hbalance rw [measureReal_add_ennreal_smul_add Mf (Kf ∘ₘ P) (Ks ∘ₘ N) d (by simp [d]), measureReal_add_ennreal_smul_add Mt (Kf ∘ₘ N) (Ks ∘ₘ P) d (by simp [d])] at hb have hf : |(Kf ∘ₘ P).real A - (Kf ∘ₘ N).real A| ≤ tvDist P N := (abs_measureReal_sub_le_tvDist hA).trans (tvDist_bind_le P N Kf) have hs : |(Ks ∘ₘ P).real A - (Ks ∘ₘ N).real A| ≤ tvDist P N := (abs_measureReal_sub_le_tvDist hA).trans (tvDist_bind_le P N Ks) have hdnonneg : 0 ≤ d.toReal := ENNReal.toReal_nonneg rw [hd] at hb hdnonneg calc |Mf.real A - Mt.real A| = (u * ε * a / 2) * |((Ks ∘ₘ P).real A - (Ks ∘ₘ N).real A) - ((Kf ∘ₘ P).real A - (Kf ∘ₘ N).real A)| := by rw [← abs_of_nonneg (by positivity : 0 ≤ u * ε * a / 2), ← abs_mul] congr 1 linarith _ ≤ (u * ε * a / 2) * (|(Ks ∘ₘ P).real A - (Ks ∘ₘ N).real A| + |(Kf ∘ₘ P).real A - (Kf ∘ₘ N).real A|) := by gcongr exact abs_sub _ _ _ ≤ u * ε * a * tvDist P N := by nlinarith

theorem markedPoissonProductPredictive_isProbabilityMeasure (C : NormalizedFiniteSignedMomentCertificate ι L) (k : ℕ) (ε a u v κ B : ℝ) (branch : Bool) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : IsProbabilityMeasure (C.markedPoissonProductPredictive k ε a u v branch) := by letI : IsProbabilityMeasure (C.markedPoissonPredictive ε a u v branch) := C.markedPoissonPredictive_isProbabilityMeasure ε a u v κ B branch ha hκ hsupp change IsProbabilityMeasure (Measure.pi fun _ : Fin k => C.markedPoissonPredictive ε a u v branch) exact inferInstance

theorem tvDist_markedPoissonProductPredictive_le (C : NormalizedFiniteSignedMomentCertificate ι L) (k : ℕ) (ε a u v κ B δ : ℝ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) (hone : tvDist (C.markedPoissonPredictive ε a u v false) (C.markedPoissonPredictive ε a u v true) ≤ δ) : tvDist (C.markedPoissonProductPredictive k ε a u v false) (C.markedPoissonProductPredictive k ε a u v true) ≤ k * δ := by letI : IsProbabilityMeasure (C.markedPoissonPredictive ε a u v false) := C.markedPoissonPredictive_isProbabilityMeasure ε a u v κ B false ha hκ hsupp letI : IsProbabilityMeasure (C.markedPoissonPredictive ε a u v true) := C.markedPoissonPredictive_isProbabilityMeasure ε a u v κ B true ha hκ hsupp unfold markedPoissonProductPredictive calc tvDist (Measure.pi fun _ : Fin k => C.markedPoissonPredictive ε a u v false) (Measure.pi fun _ : Fin k => C.markedPoissonPredictive ε a u v true) ≤ k * tvDist (C.markedPoissonPredictive ε a u v false) (C.markedPoissonPredictive ε a u v true) := tvDist_pi_iid_le k _ _ _ ≤ k * δ := mul_le_mul_of_nonneg_left hone (Nat.cast_nonneg k)

theorem zeroInflatedPrior_isProbabilityMeasure (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : IsProbabilityMeasure (C.zeroInflatedPrior a) := by let q := ∫ p, a / (p + a) ∂C.signedMeasure.variation have hq0 : 0 ≤ q := integral_nonneg_of_ae (tilt_nonneg_ae C a κ B ha hκ hsupp) have hq1 : q ≤ 1 := by simpa [q] using integral_mono_ae (integrable_tilt C a κ B ha hκ hsupp) (integrable_const 1) (tilt_le_one_ae C a κ B ha hκ hsupp) constructor rw [zeroInflatedPrior, Measure.add_apply, withDensity_apply _ MeasurableSet.univ, Measure.smul_apply, Measure.dirac_apply_of_mem (Set.mem_univ 0), smul_eq_mul, mul_one, setLIntegral_univ, ← ofReal_integral_eq_lintegral_ofReal (integrable_tilt C a κ B ha hκ hsupp) (tilt_nonneg_ae C a κ B ha hκ hsupp)] change ofReal q + ofReal (1 - q) = 1 rw [← ENNReal.ofReal_add hq0 (sub_nonneg.mpr hq1)] simp

theorem zeroInflatedPrior_support (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∀ᵐ p ∂C.zeroInflatedPrior a, p = 0 ∨ p ∈ Icc (a / κ) B := by rw [zeroInflatedPrior, ae_add_measure_iff] constructor · exact (withDensity_absolutelyContinuous _ _).ae_le (hsupp.mono fun p hp => inr hp) · apply Measure.ae_smul_measure rw [ae_dirac_iff] · exact inl rfl · exact (measurableSet_singleton 0).union (measurableSet_Icc)

theorem integral_id_zeroInflatedPrior (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∫ p, p ∂C.zeroInflatedPrior a = a * ∫ p, p / (p + a) ∂C.signedMeasure.variation := by have hprior := integrable_id_zeroInflatedPrior C a κ B ha hκ hsupp have hleft : Integrable (fun p : ℝ => p) (C.signedMeasure.variation.withDensity (fun p => ofReal (a / (p + a)))) := by simpa [zeroInflatedPrior] using hprior.mono_measure (Measure.le_add_right (μ := C.signedMeasure.variation.withDensity (fun p => ofReal (a / (p + a)))) le_rfl) have hright : Integrable (fun p : ℝ => p) (ofReal (1 - ∫ p, a / (p + a) ∂C.signedMeasure.variation) • Measure.dirac 0) := by simpa [zeroInflatedPrior] using hprior.mono_measure (Measure.le_add_left (μ := ofReal (1 - ∫ p, a / (p + a) ∂C.signedMeasure.variation) • Measure.dirac (0 : ℝ)) le_rfl) rw [zeroInflatedPrior, integral_add_measure hleft hright, integral_withDensity_eq_integral_toReal_smul (measurable_tilt a).ennreal_ofReal (ae_of_all _ fun _ => ENNReal.ofReal_lt_top) (fun p : ℝ => p), integral_smul_measure, integral_dirac] simp only [smul_eq_mul, mul_zero, add_zero] calc ∫ p, (ofReal (a / (p + a))).toReal * p ∂C.signedMeasure.variation = ∫ p, (a / (p + a)) * p ∂C.signedMeasure.variation := by apply integral_congr_ae filter_upwards [tilt_nonneg_ae C a κ B ha hκ hsupp] with p hp rw [ENNReal.toReal_ofReal hp] _ = ∫ p, a * (p / (p + a)) ∂C.signedMeasure.variation := by apply integral_congr_ae exact ae_of_all _ fun p => by ring _ = a * ∫ p, p / (p + a) ∂C.signedMeasure.variation := by rw [integral_const_mul]

theorem integral_sq_zeroInflatedPrior_le (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∫ p, p ^ 2 ∂C.zeroInflatedPrior a ≤ B * ∫ p, p ∂C.zeroInflatedPrior a := by have hid := integrable_id_zeroInflatedPrior C a κ B ha hκ hsupp have hsq := integrable_sq_zeroInflatedPrior C a κ B ha hκ hsupp rw [← integral_const_mul] apply integral_mono_ae hsq (hid.const_mul B) filter_upwards [zeroInflatedPrior_support C a κ B ha hκ hsupp] with p hp rcases hp with rfl | hp · simp · have hp0 : 0 ≤ p := (div_pos ha hκ).le.trans hp.1 simpa [pow_two] using mul_le_mul_of_nonneg_right hp.2 hp0

theorem zeroInflatedProductPrior_isProbabilityMeasure (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (k : ℕ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : IsProbabilityMeasure (C.zeroInflatedProductPrior a k) := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := zeroInflatedPrior_isProbabilityMeasure C a κ B ha hκ hsupp change IsProbabilityMeasure (Measure.pi fun _ : Fin k => C.zeroInflatedPrior a) exact inferInstance

theorem zeroInflatedProductPrior_support (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (k : ℕ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∀ᵐ w ∂C.zeroInflatedProductPrior a k, ∀ i, w i = 0 ∨ w i ∈ Icc (a / κ) B := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := zeroInflatedPrior_isProbabilityMeasure C a κ B ha hκ hsupp rw [zeroInflatedProductPrior, ae_all_iff] intro i exact (Measure.tendsto_eval_ae_ae (μ := fun _ : Fin k => C.zeroInflatedPrior a)).eventually (zeroInflatedPrior_support C a κ B ha hκ hsupp)

theorem integral_coordinate_zeroInflatedProductPrior (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (k : ℕ) (i : Fin k) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∫ w, w i ∂C.zeroInflatedProductPrior a k = a * ∫ p, p / (p + a) ∂C.signedMeasure.variation := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := zeroInflatedPrior_isProbabilityMeasure C a κ B ha hκ hsupp rw [zeroInflatedProductPrior, integral_comp_eval (μ := fun _ : Fin k => C.zeroInflatedPrior a) (f := fun p : ℝ => p) measurable_id.aestronglyMeasurable] exact integral_id_zeroInflatedPrior C a κ B ha hκ hsupp

theorem integral_coordinate_sq_zeroInflatedProductPrior (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (k : ℕ) (i : Fin k) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∫ w, (w i) ^ 2 ∂C.zeroInflatedProductPrior a k = ∫ p, p ^ 2 ∂C.zeroInflatedPrior a := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := zeroInflatedPrior_isProbabilityMeasure C a κ B ha hκ hsupp rw [zeroInflatedProductPrior, integral_comp_eval (μ := fun _ : Fin k => C.zeroInflatedPrior a) (f := fun p : ℝ => p ^ 2) (measurable_id.pow_const 2).aestronglyMeasurable]

theorem variance_coordinate_zeroInflatedProductPrior (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (k : ℕ) (i : Fin k) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : variance (fun w : Fin k → ℝ => w i) (C.zeroInflatedProductPrior a k) = variance id (C.zeroInflatedPrior a) := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := zeroInflatedPrior_isProbabilityMeasure C a κ B ha hκ hsupp change variance (id ∘ Function.eval i) (Measure.pi fun _ : Fin k => C.zeroInflatedPrior a) = variance id (C.zeroInflatedPrior a) calc _ = variance id (Measure.map (Function.eval i) (Measure.pi fun _ : Fin k => C.zeroInflatedPrior a)) := (variance_map measurable_id.aemeasurable (measurable_pi_apply i).aemeasurable).symm _ = variance id (C.zeroInflatedPrior a) := by rw [(measurePreserving_eval (fun _ : Fin k => C.zeroInflatedPrior a) i).map_eq]

theorem integral_sum_zeroInflatedProductPrior (C : NormalizedFiniteSignedMomentCertificate ι L) (a κ B : ℝ) (k : ℕ) (ha : 0 < a) (hκ : 0 < κ) (hsupp : ∀ᵐ p ∂C.signedMeasure.variation, p ∈ Icc (a / κ) B) : ∫ w, ∑ i, w i ∂C.zeroInflatedProductPrior a k = k * (a * ∫ p, p / (p + a) ∂C.signedMeasure.variation) := by letI : IsProbabilityMeasure (C.zeroInflatedPrior a) := zeroInflatedPrior_isProbabilityMeasure C a κ B ha hκ hsupp rw [zeroInflatedProductPrior] calc (∫ w, ∑ i, w i ∂Measure.pi fun _ : Fin k => C.zeroInflatedPrior a) = ∑ i, ∫ w, w i ∂Measure.pi fun _ : Fin k => C.zeroInflatedPrior a := by simpa using (integral_finsetSum univ (μ := Measure.pi fun _ : Fin k => C.zeroInflatedPrior a) (f := fun (i : Fin k) (w : Fin k → ℝ) => w i) (fun i _ => integrable_comp_eval (μ := fun _ : Fin k => C.zeroInflatedPrior a) (integrable_id_zeroInflatedPrior C a κ B ha hκ hsupp))) _ = k * (a * ∫ p, p / (p + a) ∂C.signedMeasure.variation) := by simp_rw [integral_comp_eval (μ := fun _ : Fin k => C.zeroInflatedPrior a) (f := fun p : ℝ => p) measurable_id.aestronglyMeasurable, integral_id_zeroInflatedPrior C a κ B ha hκ hsupp, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]