Stat.Minimax.Moment­Matched­Mixture

theorem exponentialPriorEnergy_quadratic_le_tail (π0 π1 : Measure ℝ) [IsProbabilityMeasure π0] [IsProbabilityMeasure π1] (lambda a : ℝ) (degree : ℕ) (hlambda : 0 ≤ lambda) (ha : 0 ≤ a) (hsupp0 : π0 {θ | |θ| ≤ a} = 1) (hsupp1 : π1 {θ | |θ| ≤ a} = 1) (hmom : ∀ n ≤ degree, priorMoment π0 n = priorMoment π1 n) : exponentialPriorEnergy π0 π0 lambda - exponentialPriorEnergy π0 π1 lambda - exponentialPriorEnergy π1 π0 lambda + exponentialPriorEnergy π1 π1 lambda ≤ 4 * exponentialSeriesTail degree (lambda * a ^ 2) := by rw [exponentialPriorEnergy_quadratic_eq_tsum π0 π1 lambda a hlambda ha hsupp0 hsupp1, exponentialSeriesTail] have h00 := summable_priorMoment_product π0 π0 lambda a hlambda ha hsupp0 hsupp0 have h01 := summable_priorMoment_product π0 π1 lambda a hlambda ha hsupp0 hsupp1 have h10 := summable_priorMoment_product π1 π0 lambda a hlambda ha hsupp1 hsupp0 have h11 := summable_priorMoment_product π1 π1 lambda a hlambda ha hsupp1 hsupp1 have hseries : Summable fun n : ℕ ↦ lambda ^ n / (n.factorial : ℝ) * (priorMoment π0 n - priorMoment π1 n) ^ 2 := by apply (((h00.sub h01).sub h10).add h11).congr intro n ring have htail : Summable fun n : ℕ ↦ if degree < n then (lambda * a ^ 2) ^ n / (n.factorial : ℝ) else 0 := by apply Summable.of_nonneg_of_le (fun n ↦ by by_cases hn : degree < n · simp only [if_pos hn] positivity · simp only [if_neg hn] positivity) (fun n ↦ by by_cases hn : degree < n · simp only [if_pos hn] exact le_rfl · simp only [if_neg hn] positivity) (Real.summable_pow_div_factorial (lambda * a ^ 2)) have hbound (n : ℕ) : lambda ^ n / (n.factorial : ℝ) * (priorMoment π0 n - priorMoment π1 n) ^ 2 ≤ 4 * (if degree < n then (lambda * a ^ 2) ^ n / (n.factorial : ℝ) else 0) := by by_cases hn : degree < n · rw [if_pos hn] have h0 := abs_priorMoment_le_pow_of_supported π0 a n ha hsupp0 have h1 := abs_priorMoment_le_pow_of_supported π1 a n ha hsupp1 have hdiff : |priorMoment π0 n - priorMoment π1 n| ≤ 2 * a ^ n := by calc |priorMoment π0 n - priorMoment π1 n| ≤ |priorMoment π0 n| + |priorMoment π1 n| := abs_sub _ _ _ ≤ a ^ n + a ^ n := add_le_add h0 h1 _ = 2 * a ^ n := by ring have hsq : (priorMoment π0 n - priorMoment π1 n) ^ 2 ≤ (2 * a ^ n) ^ 2 := (sq_le_sq).2 (by rw [abs_of_nonneg (mul_nonneg (by norm_num) (pow_nonneg ha n))] exact hdiff) calc lambda ^ n / (n.factorial : ℝ) * (priorMoment π0 n - priorMoment π1 n) ^ 2 ≤ lambda ^ n / (n.factorial : ℝ) * (2 * a ^ n) ^ 2 := by exact mul_le_mul_of_nonneg_left hsq (by positivity) _ = 4 * ((lambda * a ^ 2) ^ n / (n.factorial : ℝ)) := by ring · have hndeg : n ≤ degree := by omega simp [hn, hmom n hndeg] have hscaled := htail.mul_left 4 have hle := hseries.tsum_le_tsum hbound hscaled simpa only [tsum_mul_left] using hle

theorem momentMatchedMixture_tv_le_sqrt_tail (π0 π1 : Measure ℝ) (K : Kernel ℝ X) (Q : Measure X) (likelihood : ℝ → X → ℝ) [IsProbabilityMeasure π0] [IsProbabilityMeasure π1] [IsProbabilityMeasure Q] (hK : ∀ θ, IsProbabilityMeasure (K θ)) (lambda a : ℝ) (degree : ℕ) (hlambda : 0 ≤ lambda) (ha : 0 ≤ a) (hmeas : Measurable fun p : ℝ × X => likelihood p.1 p.2) (hnonneg : ∀ θ x, 0 ≤ likelihood θ x) (hdensity : ∀ θ, K θ = Q.withDensity fun x => ofReal (likelihood θ x)) (hinner : ∀ θ θ', ∫ x, likelihood θ x * likelihood θ' x ∂Q = exp (lambda * θ * θ')) (hsupp0 : π0 {θ | |θ| ≤ a} = 1) (hsupp1 : π1 {θ | |θ| ≤ a} = 1) (hmom : ∀ n ≤ degree, ∫ θ, θ ^ n ∂π0 = ∫ θ, θ ^ n ∂π1) : tvDist (priorPredictive π0 K) (priorPredictive π1 K) ≤ sqrt (exponentialSeriesTail degree (lambda * a ^ 2)) := by -- Rewrite both predictive measures with `priorPredictive_eq_withDensity_mixtureLikelihood`. -- Establish integrability of the squared density difference using the same four -- nonnegative cross terms as the energy identity (or an integrable pointwise upper -- bound by the sum of the two squared mixture likelihoods). Then combine -- `tvDist_le_half_sqrt_integral_sq_density_sub` with -- `integral_sq_mixtureLikelihood_sub_le_tail`; monotonicity of `sqrt` and -- `sqrt (4 * t) = 2 * sqrt t` finish, using nonnegativity of the series tail. have hpred (π : Measure ℝ) [IsProbabilityMeasure π] : priorPredictive π K = Q.withDensity fun x => ofReal (mixtureLikelihood π likelihood x) := by have hfiber (θ : ℝ) : ∫⁻ x, ofReal (likelihood θ x) ∂Q = 1 := by calc ∫⁻ x, ofReal (likelihood θ x) ∂Q = (Q.withDensity fun x => ofReal (likelihood θ x)) univ := by rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] _ = K θ univ := by rw [hdensity θ] _ = 1 := isProbabilityMeasure_iff.mp (hK θ) have hjoint : Integrable (fun p : ℝ × X => likelihood p.1 p.2) (π.prod Q) := by refine ⟨hmeas.aestronglyMeasurable, ?_⟩ apply (hasFiniteIntegral_iff_ofReal (ae_of_all _ fun p : ℝ × X => hnonneg p.1 p.2)).2 rw [lintegral_prod _ hmeas.ennreal_ofReal.aemeasurable] simp_rw [hfiber] simp have hsections : ∀ᵐ x ∂Q, Integrable (fun θ => likelihood θ x) π := hjoint.prod_left_ae have haverage : ∀ᵐ x ∂Q, ofReal (mixtureLikelihood π likelihood x) = ∫⁻ θ, ofReal (likelihood θ x) ∂π := by filter_upwards [hsections] with x hx exact ofReal_integral_eq_lintegral_ofReal hx (ae_of_all _ fun θ => hnonneg θ x) refine Measure.ext fun A hA => ?_ rw [priorPredictive_apply π K hA, withDensity_apply _ hA] simp_rw [hdensity, withDensity_apply _ hA] calc ∫⁻ θ, ∫⁻ x in A, ofReal (likelihood θ x) ∂Q ∂π = ∫⁻ x in A, ∫⁻ θ, ofReal (likelihood θ x) ∂π ∂Q := by apply lintegral_lintegral_swap exact hmeas.ennreal_ofReal.aemeasurable _ = ∫⁻ x in A, ofReal (mixtureLikelihood π likelihood x) ∂Q := by apply lintegral_congr_ae filter_upwards [ae_restrict_of_ae haverage] with x hx exact hx.symm have hmix_meas (π : Measure ℝ) [IsProbabilityMeasure π] : Measurable (mixtureLikelihood π likelihood) := by exact hmeas.stronglyMeasurable.integral_prod_left'.measurable have hmix_nonneg (π : Measure ℝ) (x : X) : 0 ≤ mixtureLikelihood π likelihood x := integral_nonneg fun θ => hnonneg θ x have hset : MeasurableSet {θ : ℝ | |θ| ≤ a} := measurableSet_le continuous_abs.measurable measurable_const have hsupp_ae (π : Measure ℝ) [IsProbabilityMeasure π] (hsupp : π {θ | |θ| ≤ a} = 1) : ∀ᵐ θ ∂π, |θ| ≤ a := by change {θ : ℝ | |θ| ≤ a} ∈ ae π rw [mem_ae_iff, measure_compl hset (measure_ne_top π _), measure_univ, hsupp, tsub_self] have hprod_int (θ θ' : ℝ) : Integrable (fun x => likelihood θ x * likelihood θ' x) Q := by by_contra h have heq := hinner θ θ' rw [integral_undef h] at heq exact Real.exp_ne_zero _ heq.symm have hmix_sq_int (π : Measure ℝ) [IsProbabilityMeasure π] (hsupp : π {θ | |θ| ≤ a} = 1) : Integrable (fun x => mixtureLikelihood π likelihood x * mixtureLikelihood π likelihood x) Q := by let g : (ℝ × ℝ) × X → ℝ := fun z => likelihood z.1.1 z.2 * likelihood z.1.2 z.2 have hgmeas : Measurable g := by unfold g fun_prop have hpairs : ∀ᵐ z ∂π.prod π, |z.1| ≤ a ∧ |z.2| ≤ a := by apply (Measure.ae_prod_iff_ae_ae ((measurableSet_le (continuous_abs.measurable.comp measurable_fst) measurable_const).inter (measurableSet_le (continuous_abs.measurable.comp measurable_snd) measurable_const))).2 filter_upwards [hsupp_ae π hsupp] with θ hθ filter_upwards [hsupp_ae π hsupp] with θ' hθ' exact ⟨hθ, hθ'⟩ have hexp_int : Integrable (fun z : ℝ × ℝ => exp (lambda * z.1 * z.2)) (π.prod π) := by apply (integrable_const (μ := π.prod π) (exp (lambda * a ^ 2))).mono' (by fun_prop) filter_upwards [hpairs] with z hz rcases hz with ⟨hz1, hz2⟩ rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] apply Real.exp_le_exp.mpr calc lambda * z.1 * z.2 ≤ |lambda * z.1 * z.2| := le_abs_self _ _ = lambda * |z.1| * |z.2| := by rw [abs_mul, abs_mul, abs_of_nonneg hlambda] _ ≤ lambda * a * a := by gcongr _ = lambda * a ^ 2 := by ring have hg_int : Integrable g ((π.prod π).prod Q) := by rw [integrable_prod_iff hgmeas.aestronglyMeasurable] constructor · filter_upwards with z simpa [g] using hprod_int z.1 z.2 · convert hexp_int using 1 funext z calc ∫ x, ‖g (z, x)‖ ∂Q = ∫ x, likelihood z.1 x * likelihood z.2 x ∂Q := by apply integral_congr_ae filter_upwards with x simp only [g, Real.norm_eq_abs, abs_of_nonneg (mul_nonneg (hnonneg _ _) (hnonneg _ _))] _ = exp (lambda * z.1 * z.2) := hinner z.1 z.2 apply hg_int.integral_prod_right.congr filter_upwards with x change (∫ z : ℝ × ℝ, likelihood z.1 x * likelihood z.2 x ∂π.prod π) = _ exact integral_prod_mul (fun θ => likelihood θ x) (fun θ => likelihood θ x) have hsq0 := hmix_sq_int π0 hsupp0 have hsq1 := hmix_sq_int π1 hsupp1 have hmajorant : Integrable (fun x => 2 * (mixtureLikelihood π0 likelihood x * mixtureLikelihood π0 likelihood x + mixtureLikelihood π1 likelihood x * mixtureLikelihood π1 likelihood x)) Q := (hsq0.add hsq1).const_mul 2 have hdiff_sq : Integrable (fun x => (mixtureLikelihood π0 likelihood x - mixtureLikelihood π1 likelihood x) ^ 2) Q := by apply hmajorant.mono' ((hmix_meas π0).sub (hmix_meas π1) |>.pow_const 2).aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] simp only [Pi.sub_apply] nlinarith [sq_nonneg (mixtureLikelihood π0 likelihood x + mixtureLikelihood π1 likelihood x)] let t := exponentialSeriesTail degree (lambda * a ^ 2) have ht : 0 ≤ t := by unfold t exponentialSeriesTail apply tsum_nonneg intro n by_cases hn : degree < n · simp only [if_pos hn] positivity · simp only [if_neg hn] exact le_rfl letI : IsProbabilityMeasure (priorPredictive π0 K) := priorPredictive_isProbability π0 K hK letI : IsProbabilityMeasure (priorPredictive π1 K) := priorPredictive_isProbability π1 K hK have htv := tvDist_le_half_sqrt_integral_sq_density_sub (priorPredictive π0 K) (priorPredictive π1 K) Q (mixtureLikelihood π0 likelihood) (mixtureLikelihood π1 likelihood) (hmix_meas π0) (hmix_meas π1) (hmix_nonneg π0) (hmix_nonneg π1) (hpred π0) (hpred π1) hdiff_sq have htail := integral_sq_mixtureLikelihood_sub_le_tail π0 π1 Q likelihood lambda a degree hlambda ha hmeas hnonneg hinner hsupp0 hsupp1 hmom change _ ≤ sqrt t calc tvDist (priorPredictive π0 K) (priorPredictive π1 K) ≤ (1 / 2 : ℝ) * sqrt (∫ x, (mixtureLikelihood π0 likelihood x - mixtureLikelihood π1 likelihood x) ^ 2 ∂Q) := htv _ ≤ (1 / 2 : ℝ) * sqrt (4 * t) := by gcongr _ = sqrt t := by rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 4)] rw [show sqrt 4 = 2 by rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)]] ring

theorem momentMatchedProductMixture_tv_le (d : ℕ) (π0 π1 : Measure ℝ) (K : Kernel ℝ X) (Q : Measure X) (likelihood : ℝ → X → ℝ) [IsProbabilityMeasure π0] [IsProbabilityMeasure π1] [IsProbabilityMeasure Q] (hK : ∀ θ, IsProbabilityMeasure (K θ)) (lambda a : ℝ) (degree : ℕ) (hlambda : 0 ≤ lambda) (ha : 0 ≤ a) (hmeas : Measurable fun p : ℝ × X => likelihood p.1 p.2) (hnonneg : ∀ θ x, 0 ≤ likelihood θ x) (hdensity : ∀ θ, K θ = Q.withDensity fun x => ofReal (likelihood θ x)) (hinner : ∀ θ θ', ∫ x, likelihood θ x * likelihood θ' x ∂Q = exp (lambda * θ * θ')) (hsupp0 : π0 {θ | |θ| ≤ a} = 1) (hsupp1 : π1 {θ | |θ| ≤ a} = 1) (hmom : ∀ n ≤ degree, ∫ θ, θ ^ n ∂π0 = ∫ θ, θ ^ n ∂π1) : tvDist (productPriorPredictive d π0 K) (productPriorPredictive d π1 K) ≤ d * sqrt (exponentialSeriesTail degree (lambda * a ^ 2)) := by -- This is the direct composition of `tvDist_pi_iid_le` and -- `momentMatchedMixture_tv_le_sqrt_tail`, after unfolding -- `productPriorPredictive` and multiplying by the nonnegative cast of `d`. letI : IsProbabilityMeasure (priorPredictive π0 K) := priorPredictive_isProbability π0 K hK letI : IsProbabilityMeasure (priorPredictive π1 K) := priorPredictive_isProbability π1 K hK unfold productPriorPredictive calc tvDist (Measure.pi fun _ : Fin d => priorPredictive π0 K) (Measure.pi fun _ : Fin d => priorPredictive π1 K) ≤ d * tvDist (priorPredictive π0 K) (priorPredictive π1 K) := tvDist_pi_iid_le d _ _ _ ≤ d * sqrt (exponentialSeriesTail degree (lambda * a ^ 2)) := mul_le_mul_of_nonneg_left (momentMatchedMixture_tv_le_sqrt_tail π0 π1 K Q likelihood hK lambda a degree hlambda ha hmeas hnonneg hdensity hinner hsupp0 hsupp1 hmom) (Nat.cast_nonneg d)

theorem momentMatchedProductMixture_tv_le_of_supported (d : ℕ) (π0 π1 : Measure ℝ) (K : Kernel ℝ X) (Q : Measure X) (likelihood : ℝ → X → ℝ) [IsProbabilityMeasure π0] [IsProbabilityMeasure π1] [IsProbabilityMeasure Q] (hK : ∀ θ, IsProbabilityMeasure (K θ)) (lambda a : ℝ) (degree : ℕ) (hlambda : 0 ≤ lambda) (ha : 0 ≤ a) (hmeas : Measurable fun p : ℝ × X => likelihood p.1 p.2) (hnonneg : ∀ θ, |θ| ≤ a → ∀ x, 0 ≤ likelihood θ x) (hdensity : ∀ θ, |θ| ≤ a → K θ = Q.withDensity fun x => ofReal (likelihood θ x)) (hinner : ∀ θ, |θ| ≤ a → ∀ θ', |θ'| ≤ a → ∫ x, likelihood θ x * likelihood θ' x ∂Q = exp (lambda * θ * θ')) (hsupp0 : π0 {θ | |θ| ≤ a} = 1) (hsupp1 : π1 {θ | |θ| ≤ a} = 1) (hmom : ∀ n ≤ degree, ∫ θ, θ ^ n ∂π0 = ∫ θ, θ ^ n ∂π1) : tvDist (productPriorPredictive d π0 K) (productPriorPredictive d π1 K) ≤ d * sqrt (exponentialSeriesTail degree (lambda * a ^ 2)) := by letI : IsProbabilityMeasure (priorPredictive π0 K) := priorPredictive_isProbability π0 K hK letI : IsProbabilityMeasure (priorPredictive π1 K) := priorPredictive_isProbability π1 K hK unfold productPriorPredictive calc tvDist (Measure.pi fun _ : Fin d => priorPredictive π0 K) (Measure.pi fun _ : Fin d => priorPredictive π1 K) ≤ d * tvDist (priorPredictive π0 K) (priorPredictive π1 K) := tvDist_pi_iid_le d _ _ _ ≤ d * sqrt (exponentialSeriesTail degree (lambda * a ^ 2)) := mul_le_mul_of_nonneg_left (momentMatchedMixture_tv_le_sqrt_tail_of_supported π0 π1 K Q likelihood hK lambda a degree hlambda ha hmeas hnonneg hdensity hinner hsupp0 hsupp1 hmom) (Nat.cast_nonneg d)