Stat.Minimax.Mixture.Moment­Matched.Bounded­Multivariate

theorem reweightedScalar_probability_finite_supported {a : ℝ} (ha₀ : 0 < a) (ω : Measure ℝ) [IsProbabilityMeasure ω] (hfinite : ∃ s : Finset ℝ, ω (s : Set ℝ) = 1) (hsupport : ω (Icc a 1) = 1) : IsProbabilityMeasure (reweightedScalar a ω) ∧ (∃ s : Finset ℝ, (reweightedScalar a ω) (s : Set ℝ) = 1) ∧ (reweightedScalar a ω) ({0} ∪ Icc a 1) = 1 := by let f : ℝ → ℝ := fun x => a / x have hmeas : Measurable f := by fun_prop have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := by apply ae_iff.mpr exact (prob_compl_eq_zero_iff measurableSet_Icc).2 hsupport have hbounds : ∀ᵐ x ∂ω, 0 ≤ f x ∧ f x ≤ 1 := by filter_upwards [hae] with x hx have hxpos : 0 < x := lt_of_lt_of_le ha₀ hx.1 constructor · exact div_nonneg (le_of_lt ha₀) (le_of_lt hxpos) · exact (div_le_one hxpos).2 hx.1 have hfint : Integrable f ω := by apply Integrable.of_bound hmeas.aestronglyMeasurable 1 filter_upwards [hbounds] with x hx simpa [abs_of_nonneg hx.1] using hx.2 have hmean₀ : 0 ≤ ∫ x, f x ∂ω := integral_nonneg_of_ae (hbounds.mono fun x hx => hx.1) have hmean₁ : (∫ x, f x ∂ω) ≤ 1 := by calc (∫ x, f x ∂ω) ≤ ∫ _x, (1 : ℝ) ∂ω := integral_mono_ae hfint (integrable_const 1) (hbounds.mono fun x hx => hx.2) _ = 1 := by simp have hmass : (ω.withDensity (fun x => ofReal (f x))) univ = ofReal (∫ x, f x ∂ω) := by rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] exact (ofReal_integral_eq_lintegral_ofReal hfint (hbounds.mono fun x hx => hx.1)).symm have hprob : IsProbabilityMeasure (reweightedScalar a ω) := by apply IsProbabilityMeasure.mk have hsum : ofReal (1 - ∫ x, f x ∂ω) + (ω.withDensity (fun x => ofReal (f x))) univ = 1 := by rw [hmass, ← ENNReal.ofReal_add (by linarith : 0 ≤ 1 - ∫ x, f x ∂ω) hmean₀] norm_num simpa [reweightedScalar, f] using hsum letI : IsProbabilityMeasure (reweightedScalar a ω) := hprob have hzero {s : Set ℝ} (hs : MeasurableSet s) (hω : ω s = 1) (h0 : (0 : ℝ) ∈ s) : (reweightedScalar a ω) s = 1 := by apply (prob_compl_eq_zero_iff hs).1 have hωc : ω sᶜ = 0 := (prob_compl_eq_zero_iff hs).2 hω have hdens : (ω.withDensity (fun x => ofReal (f x))) sᶜ = 0 := (withDensity_absolutelyContinuous ω (fun x => ofReal (f x))) hωc change ofReal (1 - ∫ x, f x ∂ω) • (Measure.dirac 0) sᶜ + (ω.withDensity (fun x => ofReal (f x))) sᶜ = 0 simp [hdens, h0] refine ⟨hprob, ?_, ?_⟩ · obtain ⟨s, hs⟩ := hfinite refine ⟨insert 0 s, hzero (Finset.measurableSet _) ?_ (by simp)⟩ exact le_antisymm prob_le_one (hs ▸ measure_mono (by simp)) · apply hzero (MeasurableSet.union (by simp) measurableSet_Icc) ?_ (by simp) exact le_antisymm prob_le_one (hsupport ▸ measure_mono Set.subset_union_right)

theorem integral_targetFunctional_triplePrior {a b q : ℝ} (ha : 0 < a) (hq : 0 ≤ q) (ω : Measure ℝ) [IsProbabilityMeasure ω] (hsupport : ω (Icc a 1) = 1) : (∫ t, targetFunctional t ∂triplePrior b a q ω) = a * b * ∫ x, x / (x + q * a) ∂ω := by let d : ℝ → ENNReal := fun x => ofReal (a / x) let G : ℝ → ℝ := fun x => targetFunctional (scalarToTriple b a q x) let R : ℝ → ℝ := fun x => x / (x + q * a) have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := by apply ae_iff.mpr exact (prob_compl_eq_zero_iff measurableSet_Icc).2 hsupport have hd : Measurable d := by fun_prop have hdtop : ∀ᵐ x ∂ω, d x < ⊤ := by simp [d] have hmap : Measurable (scalarToTriple b a q) := by unfold scalarToTriple apply Measurable.ite (measurableSet_singleton 0) · fun_prop · fun_prop have hG : Measurable G := by exact (show Measurable targetFunctional by unfold targetFunctional fun_prop).comp hmap have hRcont : ContinuousOn R (Icc a 1) := by dsimp [R] apply ContinuousOn.div (by fun_prop) (by fun_prop) intro x hx have hxpos : 0 < x := lt_of_lt_of_le ha hx.1 have hqa : 0 ≤ q * a := mul_nonneg hq (le_of_lt ha) positivity have hRint : Integrable R ω := by have h : IntegrableOn R (Icc a 1) ω := hRcont.integrableOn_compact isCompact_Icc have hsets : (Set.univ : Set ℝ) =ᵐ[ω] Icc a 1 := by filter_upwards [hae] with x hx exact propext (iff_of_true trivial hx) simpa using h.congr_set_ae hsets have hpoint (x : ℝ) (hx : x ∈ Icc a 1) : (d x).toReal * G x = a * b * R x := by have hxpos : 0 < x := lt_of_lt_of_le ha hx.1 have hxne : x ≠ 0 := ne_of_gt hxpos have hden : x + q * a ≠ 0 := by positivity have hadiv : 0 ≤ a / x := div_nonneg (le_of_lt ha) (le_of_lt hxpos) simp only [d, G, R, scalarToTriple, if_neg hxne, targetFunctional, ENNReal.toReal_ofReal hadiv] field_simp have hweight : Integrable (fun x => (d x).toReal * G x) ω := by have h := hRint.const_mul (a * b) exact h.congr (hae.mono fun x hx => (hpoint x hx).symm) have hdens : Integrable G (ω.withDensity d) := by exact (integrable_withDensity_iff_integrable_smul' hd hdtop).2 (by simpa only [smul_eq_mul] using hweight) have hdirac : Integrable G (Measure.dirac 0) := integrable_dirac (by simp) have hsum : Integrable G (reweightedScalar a ω) := by unfold reweightedScalar exact (hdirac.smul_measure ENNReal.ofReal_ne_top).add_measure hdens calc (∫ t, targetFunctional t ∂triplePrior b a q ω) = ∫ x, G x ∂reweightedScalar a ω := by exact integral_map hmap.aemeasurable (by unfold targetFunctional fun_prop) _ = ∫ x, G x ∂ω.withDensity d := by rw [reweightedScalar, integral_add_measure (hdirac.smul_measure ENNReal.ofReal_ne_top) hdens, integral_smul_measure, integral_dirac] simp [G, targetFunctional, scalarToTriple] _ = ∫ x, (d x).toReal * G x ∂ω := by rw [integral_withDensity_eq_integral_toReal_smul hd hdtop] simp only [smul_eq_mul] _ = ∫ x, a * b * R x ∂ω := integral_congr_ae (hae.mono fun x hx => hpoint x hx) _ = a * b * ∫ x, R x ∂ω := by rw [integral_const_mul] _ = _ := rfl

theorem predictiveLaw_isProbability (n : ℝ) (ν : Measure MarkedParam) [IsProbabilityMeasure ν] : IsProbabilityMeasure (predictiveLaw n ν) := by unfold predictiveLaw exact MeasureTheory.isProbabilityMeasure_bind (measurable_markedPoissonLaw n).aemeasurable (Filter.Eventually.of_forall fun t => by unfold markedPoissonLaw infer_instance)

theorem markedPoissonLaw_singleton {n : ℝ} (hn : 0 ≤ n) (t : MarkedParam) (hp : 0 ≤ t.1) (hπ₀ : 0 ≤ t.2.1) (hπ₁ : t.2.1 ≤ 1) (hμ₀ : 0 ≤ t.2.2) (hμ₁ : t.2.2 ≤ 1) (u v w : ℕ) : (markedPoissonLaw n t).real {((u, v), w)} = exp (-n * t.1) * (n * t.1 * t.2.1 * t.2.2) ^ u * (n * t.1 * t.2.1 * (1 - t.2.2)) ^ v * (n * t.1 * (1 - t.2.1)) ^ w / ((Nat.factorial u : ℝ) * (Nat.factorial v : ℝ) * (Nat.factorial w : ℝ)) := by have hr₁ : 0 ≤ n * t.1 * t.2.1 * t.2.2 := by positivity have hr₂ : 0 ≤ n * t.1 * t.2.1 * (1 - t.2.2) := by positivity have hr₃ : 0 ≤ n * t.1 * (1 - t.2.1) := by positivity have hmass : (markedPoissonLaw n t).real {((u, v), w)} = (poissonMeasure (nnRate (n * t.1 * t.2.1 * t.2.2))).real {u} * (poissonMeasure (nnRate (n * t.1 * t.2.1 * (1 - t.2.2)))).real {v} * (poissonMeasure (nnRate (n * t.1 * (1 - t.2.1)))).real {w} := by rw [measureReal_def, markedPoissonLaw, ← Set.singleton_prod_singleton, Measure.prod_prod, ← Set.singleton_prod_singleton, Measure.prod_prod, ENNReal.toReal_mul, ENNReal.toReal_mul] rfl rw [hmass, poissonMeasure_real_singleton, poissonMeasure_real_singleton, poissonMeasure_real_singleton] simp only [nnRate, Real.coe_toNNReal _ hr₁, Real.coe_toNNReal _ hr₂, Real.coe_toNNReal _ hr₃] have hexp : exp (-(n * t.1 * t.2.1 * t.2.2)) * exp (-(n * t.1 * t.2.1 * (1 - t.2.2))) * exp (-(n * t.1 * (1 - t.2.1))) = exp (-n * t.1) := by rw [← Real.exp_add, ← Real.exp_add] congr 1 ring rw [show -n * t.1 = -(n * t.1) by ring] at hexp field_simp rw [← hexp] ring

theorem predictiveLaw_singleton {n : ℝ} (hn : 0 ≤ n) (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hsupport : ν {t | 0 ≤ t.1 ∧ 0 ≤ t.2.1 ∧ t.2.1 ≤ 1 ∧ 0 ≤ t.2.2 ∧ t.2.2 ≤ 1} = 1) (u v w : ℕ) : (predictiveLaw n ν).real {((u, v), w)} = ∫ t, exp (-n * t.1) * (n * t.1 * t.2.1 * t.2.2) ^ u * (n * t.1 * t.2.1 * (1 - t.2.2)) ^ v * (n * t.1 * (1 - t.2.1)) ^ w / ((Nat.factorial u : ℝ) * (Nat.factorial v : ℝ) * (Nat.factorial w : ℝ)) ∂ν := by let s : Set MarkedParam := {t | 0 ≤ t.1 ∧ 0 ≤ t.2.1 ∧ t.2.1 ≤ 1 ∧ 0 ≤ t.2.2 ∧ t.2.2 ≤ 1} have hs : MeasurableSet s := by dsimp [s] measurability have hae : ∀ᵐ t ∂ν, t ∈ s := (mem_ae_iff_prob_eq_one hs).2 hsupport have hmeas : Measurable (markedPoissonLaw n) := measurable_markedPoissonLaw n have hmass_meas : AEMeasurable (fun t => markedPoissonLaw n t {((u, v), w)}) ν := ((Measure.measurable_coe (measurableSet_singleton _)).comp hmeas).aemeasurable have hmass_finite : ∀ᵐ t ∂ν, markedPoissonLaw n t {((u, v), w)} < ⊤ := Filter.Eventually.of_forall fun t => by haveI : IsProbabilityMeasure (markedPoissonLaw n t) := by unfold markedPoissonLaw infer_instance exact (measure_mono (Set.subset_univ _)).trans_lt (by simp) rw [measureReal_def, predictiveLaw, Measure.bind_apply (measurableSet_singleton _) hmeas.aemeasurable, ← integral_toReal hmass_meas hmass_finite] apply integral_congr_ae filter_upwards [hae] with t ht rcases ht with ⟨hp, hπ₀, hπ₁, hμ₀, hμ₁⟩ exact markedPoissonLaw_singleton hn t hp hπ₀ hπ₁ hμ₀ hμ₁ u v w

theorem unmatchedTail_le_factorial (K : ℕ) {n b : ℝ} (hn : 0 ≤ n) (hb : 0 ≤ b) : unmatchedTail K n b ≤ exp (2 * n * b) * (2 * n * b) ^ (3 * K + 1) / (factorial (3 * K + 1) : ℝ) := by let x : ℝ := 2 * n * b let q : ℕ := 3 * K + 1 have hx : 0 ≤ x := by dsimp [x]; positivity have hs : Summable (fun m : ℕ => x ^ m / (m.factorial : ℝ)) := Real.summable_pow_div_factorial x have hshift : Summable (fun j : ℕ => x ^ (j + q) / ((j + q).factorial : ℝ)) := (summable_nat_add_iff q).2 hs have htail : unmatchedTail K n b = ∑' j : ℕ, x ^ (j + q) / ((j + q).factorial : ℝ) := by let g : ℕ → ℝ := fun m => if q ≤ m then x ^ m / (m.factorial : ℝ) else 0 have hg : Summable (fun j : ℕ => g (j + q)) := by simpa [g] using hshift have h := hg.sum_add_tsum_nat_add' (f := g) (k := q) have hzero : (∑ i ∈ range q, g i) = 0 := by apply Finset.sum_eq_zero intro i hi simp [g, lt_of_lt_of_le (Finset.mem_range.mp hi) (le_refl q)] rw [hzero, zero_add] at h have hshiftg : (fun i => g (i + q)) = (fun i => x ^ (i + q) / ((i + q).factorial : ℝ)) := by funext i simp [g] rw [hshiftg] at h have hiff (m : ℕ) : (3 * K < m) ↔ q ≤ m := by dsimp [q]; omega simpa only [unmatchedTail, hiff, g, x] using h.symm rw [htail] have hterm (j : ℕ) : x ^ (j + q) / ((j + q).factorial : ℝ) ≤ (x ^ q / (q.factorial : ℝ)) * (x ^ j / (j.factorial : ℝ)) := by have hf : (q.factorial : ℝ) * (j.factorial : ℝ) ≤ ((q + j).factorial : ℝ) := by exact_mod_cast Nat.le_of_dvd (Nat.factorial_pos _) (Nat.factorial_mul_factorial_dvd_factorial_add q j) rw [add_comm j q, pow_add] calc x ^ q * x ^ j / ((q + j).factorial : ℝ) ≤ x ^ q * x ^ j / ((q.factorial : ℝ) * (j.factorial : ℝ)) := by gcongr _ = x ^ q / (q.factorial : ℝ) * (x ^ j / (j.factorial : ℝ)) := by ring calc (∑' j : ℕ, x ^ (j + q) / ((j + q).factorial : ℝ)) ≤ ∑' j : ℕ, (x ^ q / (q.factorial : ℝ)) * (x ^ j / (j.factorial : ℝ)) := by exact Summable.tsum_le_tsum (fun j => hterm j) hshift (hs.mul_left _) _ = exp x * x ^ q / (q.factorial : ℝ) := by rw [tsum_mul_left, Real.exp_eq_exp_ℝ, NormedSpace.exp_eq_tsum_div] ring

theorem integral_markedRateProduct_match {K : ℕ} {b ε gap : ℝ} (T : TriplePriors K b ε gap) (t u v w : ℕ) (hdegree : t + u + v + w ≤ 3 * K) : (∫ θ : MarkedParam, θ.1 ^ t * (θ.1 * θ.2.1 * θ.2.2) ^ u * (θ.1 * θ.2.1 * (1 - θ.2.2)) ^ v * (θ.1 * (1 - θ.2.1)) ^ w ∂T.ν₀) = (∫ θ : MarkedParam, θ.1 ^ t * (θ.1 * θ.2.1 * θ.2.2) ^ u * (θ.1 * θ.2.1 * (1 - θ.2.2)) ^ v * (θ.1 * (1 - θ.2.1)) ^ w ∂T.ν₁) := by let F (i j k a c : ℕ) (θ : MarkedParam) : ℝ := θ.1 ^ i * (θ.1 * θ.2.1) ^ j * (θ.1 * θ.2.1 * θ.2.2) ^ k * (θ.1 * θ.2.1 * (1 - θ.2.2)) ^ a * (θ.1 * (1 - θ.2.1)) ^ c have integrable_F (μ : Measure MarkedParam) [IsProbabilityMeasure μ] (hfin : ∃ s : Finset MarkedParam, μ (s : Set MarkedParam) = 1) (i j k a c : ℕ) : Integrable (F i j k a c) μ := by obtain ⟨s, hs⟩ := hfin let cell : (s : Set MarkedParam) ↪ MarkedParam := ⟨Subtype.val, Subtype.val_injective⟩ have hrange : μ (range cell) = μ univ := by have heq : range cell = (s : Set MarkedParam) := by ext θ simp [cell] rw [heq, hs] simp apply integrable_of_finite_atomic_support μ cell (fun _ => measurableSet_singleton _) hrange dsimp [F] fun_prop haveI := T.probability₀ haveI := T.probability₁ have hmatch₀ : ∀ i j k a, i + j + k + a ≤ 3 * K → (∫ θ, F i j k a 0 θ ∂T.ν₀) = ∫ θ, F i j k a 0 θ ∂T.ν₁ := by intro i j k a induction a generalizing i j k with | zero => intro hd simpa [F, mixedMonomial] using T.mixed_match i j k (by omega) | succ a ih => intro hd have hp (θ : MarkedParam) : F i j k (a + 1) 0 θ = F i (j + 1) k a 0 θ - F i j (k + 1) a 0 θ := by dsimp [F] rw [pow_succ, pow_succ, pow_succ] ring have hleft : i + (j + 1) + k + a ≤ 3 * K := by omega have hright : i + j + (k + 1) + a ≤ 3 * K := by omega calc (∫ θ, F i j k (a + 1) 0 θ ∂T.ν₀) = ∫ θ, F i (j + 1) k a 0 θ - F i j (k + 1) a 0 θ ∂T.ν₀ := by apply integral_congr_ae filter_upwards [] with θ exact hp θ _ = (∫ θ, F i (j + 1) k a 0 θ ∂T.ν₀) - (∫ θ, F i j (k + 1) a 0 θ ∂T.ν₀) := by rw [integral_sub (integrable_F T.ν₀ T.finite₀ _ _ _ _ _) (integrable_F T.ν₀ T.finite₀ _ _ _ _ _)] _ = (∫ θ, F i (j + 1) k a 0 θ ∂T.ν₁) - (∫ θ, F i j (k + 1) a 0 θ ∂T.ν₁) := by rw [ih _ _ _ hleft, ih _ _ _ hright] _ = ∫ θ, F i j k (a + 1) 0 θ ∂T.ν₁ := by rw [← integral_sub (integrable_F T.ν₁ T.finite₁ _ _ _ _ _) (integrable_F T.ν₁ T.finite₁ _ _ _ _ _)] apply integral_congr_ae filter_upwards [] with θ exact (hp θ).symm have hmatch : ∀ c i j k a, i + j + k + a + c ≤ 3 * K → (∫ θ, F i j k a c θ ∂T.ν₀) = ∫ θ, F i j k a c θ ∂T.ν₁ := by intro c induction c with | zero => intro i j k a hd exact hmatch₀ i j k a (by omega) | succ c ih => intro i j k a hd have hp (θ : MarkedParam) : F i j k a (c + 1) θ = F (i + 1) j k a c θ - F i (j + 1) k a c θ := by dsimp [F] rw [pow_succ, pow_succ, pow_succ] ring have hleft : (i + 1) + j + k + a + c ≤ 3 * K := by omega have hright : i + (j + 1) + k + a + c ≤ 3 * K := by omega calc (∫ θ, F i j k a (c + 1) θ ∂T.ν₀) = ∫ θ, F (i + 1) j k a c θ - F i (j + 1) k a c θ ∂T.ν₀ := by apply integral_congr_ae filter_upwards [] with θ exact hp θ _ = (∫ θ, F (i + 1) j k a c θ ∂T.ν₀) - (∫ θ, F i (j + 1) k a c θ ∂T.ν₀) := by rw [integral_sub (integrable_F T.ν₀ T.finite₀ _ _ _ _ _) (integrable_F T.ν₀ T.finite₀ _ _ _ _ _)] _ = (∫ θ, F (i + 1) j k a c θ ∂T.ν₁) - (∫ θ, F i (j + 1) k a c θ ∂T.ν₁) := by rw [ih _ _ _ _ hleft, ih _ _ _ _ hright] _ = ∫ θ, F i j k a (c + 1) θ ∂T.ν₁ := by rw [← integral_sub (integrable_F T.ν₁ T.finite₁ _ _ _ _ _) (integrable_F T.ν₁ T.finite₁ _ _ _ _ _)] apply integral_congr_ae filter_upwards [] with θ exact (hp θ).symm simpa [F] using hmatch w t 0 u v (by omega)

theorem abs_predictiveLaw_singleton_diff_le_unmatchedEnvelope {K : ℕ} {b ε gap n : ℝ} (hn : 0 ≤ n) (hε : 0 ≤ ε) (T : TriplePriors K b ε gap) (u v w : ℕ) : |(predictiveLaw n T.ν₀).real {((u, v), w)} - (predictiveLaw n T.ν₁).real {((u, v), w)}| ≤ ∑' t : ℕ, if 3 * K < t + u + v + w then (∫ θ, markedEnvelopeCoeff n θ t u v w ∂T.ν₀) + (∫ θ, markedEnvelopeCoeff n θ t u v w ∂T.ν₁) else 0 := by haveI := T.probability₀ haveI := T.probability₁ let E (t : ℕ) (θ : MarkedParam) : ℝ := markedEnvelopeCoeff n θ t u v w let P (t : ℕ) (θ : MarkedParam) : ℝ := θ.1 ^ t * (θ.1 * θ.2.1 * θ.2.2) ^ u * (θ.1 * θ.2.1 * (1 - θ.2.2)) ^ v * (θ.1 * (1 - θ.2.1)) ^ w let A (ν : Measure MarkedParam) (t : ℕ) : ℝ := (-1 : ℝ) ^ t * ∫ θ, E t θ ∂ν have hErepr (t : ℕ) (θ : MarkedParam) : E t θ = (n ^ (t + u + v + w) / ((Nat.factorial t : ℝ) * (Nat.factorial u : ℝ) * (Nat.factorial v : ℝ) * (Nat.factorial w : ℝ))) * P t θ := by dsimp [E, P] simp only [markedEnvelopeCoeff, mul_pow, pow_add] ring have hsum_integral (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hfinite : ∃ s : Finset MarkedParam, ν (s : Set MarkedParam) = 1) (F : ℕ → MarkedParam → ℝ) (hF : ∀ t, StronglyMeasurable (F t)) (hs : ∀ θ, Summable (fun t => F t θ)) : Summable (fun t => ∫ θ, F t θ ∂ν) := by obtain ⟨s, hsμ⟩ := hfinite let cell : (s : Set MarkedParam) ↪ MarkedParam := ⟨Subtype.val, Subtype.val_injective⟩ have hrange : ν (range cell) = ν univ := by have heq : range cell = (s : Set MarkedParam) := by ext θ simp [cell] rw [heq, hsμ] simp have hν := measure_eq_fin_sum_smul_dirac_of_range ν cell (fun _ => measurableSet_singleton _) hrange have hint (t : ℕ) : (∫ θ, F t θ ∂ν) = ∑ i : (s : Set MarkedParam), (ν {cell i}).toReal * F t (cell i) := by conv_lhs => rw [hν] rw [integral_finsetSum_measure (by intro i hi exact (integrable_dirac' (hF t) (by simp)).smul_measure (measure_ne_top ν {cell i}))] simp only [integral_smul_measure, integral_dirac' _ _ (hF t), smul_eq_mul] simp_rw [hint] classical have hsum : ∀ q : Finset (s : Set MarkedParam), Summable (fun t => ∑ i ∈ q, (ν {cell i}).toReal * F t (cell i)) := by intro q induction q using Finset.induction_on with | empty => simp | @insert a q ha ih => simp only [Finset.sum_insert ha] exact ((hs (cell a)).mul_left _).add ih simpa only [Finset.sum_attach] using hsum univ have hEpoint (θ : MarkedParam) : Summable (fun t => E t θ) := by have h := (Real.summable_pow_div_factorial (n * θ.1)).mul_right (((n * θ.1 * θ.2.1 * θ.2.2) ^ u / (Nat.factorial u : ℝ)) * ((n * θ.1 * θ.2.1 * (1 - θ.2.2)) ^ v / (Nat.factorial v : ℝ)) * ((n * θ.1 * (1 - θ.2.1)) ^ w / (Nat.factorial w : ℝ))) simpa only [E, markedEnvelopeCoeff, mul_assoc, div_eq_mul_inv] using h have hEmeas (t : ℕ) : StronglyMeasurable (E t) := by dsimp [E, markedEnvelopeCoeff] fun_prop have hsumE₀ : Summable (fun t => ∫ θ, E t θ ∂T.ν₀) := hsum_integral T.ν₀ T.finite₀ E hEmeas hEpoint have hsumE₁ : Summable (fun t => ∫ θ, E t θ ∂T.ν₁) := hsum_integral T.ν₁ T.finite₁ E hEmeas hEpoint have hsupport (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hs : ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ ε ≤ θ.2.1 ∧ θ.2.1 ≤ 1 - ε ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} = 1) : ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} = 1 := by apply le_antisymm · calc ν {θ : MarkedParam | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} ≤ ν univ := measure_mono (Set.subset_univ _) _ = 1 := measure_univ · calc (1 : ENNReal) = ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ ε ≤ θ.2.1 ∧ θ.2.1 ≤ 1 - ε ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} := hs.symm _ ≤ _ := measure_mono (by intro θ hθ rcases hθ with ⟨hp₀, hp₁, hπ₀, hπ₁, hμ₀, hμ₁⟩ exact ⟨hp₀, hp₁, hε.trans hπ₀, hπ₁.trans (sub_le_self 1 hε), hμ₀, hμ₁⟩) have hs₀ := hsupport T.ν₀ T.supported₀ have hs₁ := hsupport T.ν₁ T.supported₁ have hEnonneg (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hs : ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} = 1) (t : ℕ) : 0 ≤ ∫ θ, E t θ ∂ν := by apply integral_nonneg_of_ae have hae : ∀ᵐ θ ∂ν, θ ∈ {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} := (mem_ae_iff_prob_eq_one (by measurability)).2 hs filter_upwards [hae] with θ hθ rcases hθ with ⟨hp₀, hp₁, hπ₀, hπ₁, hμ₀, hμ₁⟩ dsimp [E, markedEnvelopeCoeff] positivity have hAabs (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hs : ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} = 1) (t : ℕ) : |A ν t| = ∫ θ, E t θ ∂ν := by dsimp [A] rw [abs_mul, abs_pow, abs_neg, abs_one, one_pow, one_mul, abs_of_nonneg (hEnonneg ν hs t)] have hsumA₀ : Summable (A T.ν₀) := by apply Summable.of_abs simpa only [hAabs T.ν₀ hs₀] using hsumE₀ have hsumA₁ : Summable (A T.ν₁) := by apply Summable.of_abs simpa only [hAabs T.ν₁ hs₁] using hsumE₁ have hcoef (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (t : ℕ) : ((-n) ^ t * n ^ (u + v + w) / ((Nat.factorial t : ℝ) * (Nat.factorial u : ℝ) * (Nat.factorial v : ℝ) * (Nat.factorial w : ℝ))) * (∫ θ, P t θ ∂ν) = A ν t := by have hi : (∫ θ, E t θ ∂ν) = (n ^ (t + u + v + w) / ((Nat.factorial t : ℝ) * (Nat.factorial u : ℝ) * (Nat.factorial v : ℝ) * (Nat.factorial w : ℝ))) * (∫ θ, P t θ ∂ν) := by simp_rw [hErepr, integral_const_mul] change _ = (-1 : ℝ) ^ t * ∫ θ, E t θ ∂ν rw [hi, show -n = (-1 : ℝ) * n by ring, mul_pow] simp only [pow_add] ring have hpred (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hfinite : ∃ s : Finset MarkedParam, ν (s : Set MarkedParam) = 1) (hs : ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} = 1) : (predictiveLaw n ν).real {((u, v), w)} = ∑' t, A ν t := by rw [predictiveLaw_singleton_eq_tsum_markedRateProduct hn ν hfinite hs u v w] apply tsum_congr intro t exact hcoef ν t have hmatch (t : ℕ) (hd : t + u + v + w ≤ 3 * K) : A T.ν₀ t = A T.ν₁ t := by dsimp [A] congr 1 simp_rw [hErepr, integral_const_mul] congr 1 exact integral_markedRateProduct_match T t u v w hd let D (t : ℕ) : ℝ := A T.ν₀ t - A T.ν₁ t let B (t : ℕ) : ℝ := (∫ θ, E t θ ∂T.ν₀) + (∫ θ, E t θ ∂T.ν₁) have hsumD : Summable D := hsumA₀.sub hsumA₁ have hsumB : Summable B := hsumE₀.add hsumE₁ have hbound (t : ℕ) : |D t| ≤ B t := by dsimp [D, B] calc |A T.ν₀ t - A T.ν₁ t| ≤ |A T.ν₀ t| + |A T.ν₁ t| := abs_sub _ _ _ = (∫ θ, E t θ ∂T.ν₀) + (∫ θ, E t θ ∂T.ν₁) := by rw [hAabs T.ν₀ hs₀ t, hAabs T.ν₁ hs₁ t] have hsumDt : Summable (fun t => if 3 * K < t + u + v + w then D t else 0) := by have hi := hsumD.indicator {t | 3 * K < t + u + v + w} have heq : (fun t => if 3 * K < t + u + v + w then D t else 0) = indicator {t | 3 * K < t + u + v + w} D := by funext t simp [Set.indicator_apply] rw [heq] exact hi have hsumBt : Summable (fun t => if 3 * K < t + u + v + w then B t else 0) := by have hi := hsumB.indicator {t | 3 * K < t + u + v + w} have heq : (fun t => if 3 * K < t + u + v + w then B t else 0) = indicator {t | 3 * K < t + u + v + w} B := by funext t simp [Set.indicator_apply] rw [heq] exact hi calc |(predictiveLaw n T.ν₀).real {((u, v), w)} - (predictiveLaw n T.ν₁).real {((u, v), w)}| = |∑' t, D t| := by rw [hpred T.ν₀ T.finite₀ hs₀, hpred T.ν₁ T.finite₁ hs₁] rw [← hsumA₀.tsum_sub hsumA₁] _ = |∑' t, if 3 * K < t + u + v + w then D t else 0| := by congr 1 apply tsum_congr intro t by_cases ht : 3 * K < t + u + v + w · simp [ht] · simp [ht, D, hmatch t (by omega)] _ ≤ ∑' t, |if 3 * K < t + u + v + w then D t else 0| := by have hnorm : Summable (fun t => ‖if 3 * K < t + u + v + w then D t else 0‖) := by simpa only [Real.norm_eq_abs] using hsumDt.abs simpa only [Real.norm_eq_abs] using (norm_tsum_le_tsum_norm (f := fun t => if 3 * K < t + u + v + w then D t else 0) hnorm) _ ≤ ∑' t, if 3 * K < t + u + v + w then B t else 0 := by apply hsumDt.abs.tsum_le_tsum · intro t by_cases ht : 3 * K < t + u + v + w · simpa only [if_pos ht] using hbound t · simp [ht] · exact hsumBt _ = _ := rfl

theorem exists_scalarPriors_of_inverseGap {q c₀ δ : ℝ} (hq₀ : 0 < q) (hc₀ : 0 < c₀) (hδ : 0 < δ) (happrox : ∀ K : ℕ, 1 ≤ K → ∀ α : ℝ, ∀ P : Polynomial ℝ, P.natDegree ≤ 3 * K → ∃ x ∈ Icc (endpointScale c₀ K) 1, δ ≤ |x / (x + q * endpointScale c₀ K) - (α / x + P.eval x)|) : ∀ K : ℕ, 1 ≤ K → Nonempty (ScalarPriors K (endpointScale c₀ K) q δ) := by intro K hK classical let a := endpointScale c₀ K have hKpos : (0 : ℝ) < K := by exact_mod_cast (Nat.zero_lt_of_lt hK) have ha : 0 < a := by dsimp [a, endpointScale] positivity let f : ℝ → ℝ := fun x => x / (x + q * a) let g : Fin (3 * K + 2) → ℝ → ℝ := fun i x => if i = 0 then x⁻¹ else x ^ (i.val - 1) have hf : ContinuousOn f (Icc a 1) := by apply continuousOn_id.div (continuousOn_id.add continuousOn_const) intro x hx have hxpos : 0 < x := lt_of_lt_of_le ha hx.1 have hqa : 0 ≤ q * a := mul_nonneg hq₀.le ha.le change x + q * a ≠ 0 positivity have hg : ∀ i, ContinuousOn (g i) (Icc a 1) := by intro i by_cases hi : i = 0 · subst i change ContinuousOn (fun x : ℝ => x⁻¹) (Icc a 1) apply continuousOn_id.inv₀ intro x hx exact ne_of_gt (lt_of_lt_of_le ha hx.1) · simp only [g, if_neg hi] exact continuousOn_id.pow _ have hgap : ∀ α : ℝ, ∀ c : Fin (3 * K + 2) → ℝ, ∃ x ∈ Icc a 1, δ ≤ |f x - (α + ∑ i, c i * g i x)| := by intro α c let P : Polynomial ℝ := C α + ∑ j : Fin (3 * K + 1), C (c j.succ) * X ^ j.val have hP : P.natDegree ≤ 3 * K := by dsimp [P] apply (Polynomial.natDegree_add_le _ _).trans apply max_le · simp · apply Polynomial.natDegree_sum_le_of_forall_le intro j hj exact (Polynomial.natDegree_C_mul_X_pow_le (c j.succ) j.val).trans (le_of_lt_succ j.isLt) obtain ⟨x, hx, hδx⟩ := happrox K hK (c 0) P hP refine ⟨x, hx, ?_⟩ have hsum : (∑ i : Fin (3 * K + 2), c i * g i x) = c 0 / x + ∑ j : Fin (3 * K + 1), c j.succ * x ^ j.val := by rw [Fin.sum_univ_succ] simp [g, div_eq_mul_inv] have hPeval : P.eval x = α + ∑ j : Fin (3 * K + 1), c j.succ * x ^ j.val := by simp [P, Polynomial.eval_finsetSum] rw [hsum] rw [hPeval] at hδx have hform : α + (c 0 / x + ∑ j : Fin (3 * K + 1), c j.succ * x ^ j.val) = c 0 / x + (α + ∑ j : Fin (3 * K + 1), c j.succ * x ^ j.val) := by ring rw [hform] simpa only [f, a] using hδx obtain ⟨ω₀, ω₁, hp₀, hp₁, hfin₀, hfin₁, hs₀, hs₁, hmatch, htarget⟩ := exists_finitePriors_of_constrainedApproxGap hδ f g hf hg hgap refine ⟨{ positive_degree := hK, ω₀ := ω₀, ω₁ := ω₁, probability₀ := hp₀, probability₁ := hp₁, finite₀ := hfin₀, finite₁ := hfin₁, supported₀ := hs₀, supported₁ := hs₁, inverse_match := ?_, ordinary_match := ?_, target_gap := htarget }⟩ · exact hmatch 0 · intro m hm let j : Fin (3 * K + 1) := ⟨m, by omega⟩ have h := hmatch j.succ simpa [g, j] using h

theorem exists_matching_convexHull_features_of_gap {m : ℕ} {r s δ : ℝ} (hδ : 0 < δ) (f : ℝ → ℝ) (g : Fin m → ℝ → ℝ) (hf : ContinuousOn f (Icc r s)) (hg : ∀ i, ContinuousOn (g i) (Icc r s)) (hgap : ∀ α : ℝ, ∀ c : Fin m → ℝ, ∃ x ∈ Icc r s, δ ≤ |f x - (α + ∑ i, c i * g i x)|) : ∃ y₀ y₁ : ℝ × (Fin m → ℝ), y₀ ∈ convexHull ℝ ((fun x : ℝ => (f x, fun i => g i x)) '' Icc r s) ∧ y₁ ∈ convexHull ℝ ((fun x : ℝ => (f x, fun i => g i x)) '' Icc r s) ∧ y₀.2 = y₁.2 ∧ δ ≤ |y₀.1 - y₁.1| := by have hF : ContinuousOn (fun x : ℝ => (f x, fun i => g i x)) (Icc r s) := hf.prodMk (continuousOn_pi.mpr hg) have hS : IsCompact ((fun x : ℝ => (f x, fun i => g i x)) '' Icc r s) := isCompact_Icc.image_of_continuousOn hF apply exists_matching_convexHull_of_compact_feature_gap hS hδ intro α c obtain ⟨x, hx, herror⟩ := hgap α c exact ⟨(f x, fun i => g i x), ⟨x, hx, rfl⟩, herror⟩

theorem finitePrior_of_convexHull_features {m : ℕ} {r s : ℝ} (f : ℝ → ℝ) (g : Fin m → ℝ → ℝ) (y : ℝ × (Fin m → ℝ)) (hy : y ∈ convexHull ℝ ((fun x : ℝ => (f x, fun i => g i x)) '' Icc r s)) : ∃ ω : Measure ℝ, IsProbabilityMeasure ω ∧ (∃ t : Finset ℝ, ω (t : Set ℝ) = 1) ∧ ω (Icc r s) = 1 ∧ (∫ x, f x ∂ω) = y.1 ∧ (∀ i, (∫ x, g i x ∂ω) = y.2 i) := by classical obtain ⟨ι, hι, w, z, hw₀, hw₁, hz, hsum⟩ := (mem_convexHull_iff_exists_fintype (R := ℝ)).mp hy letI : Fintype ι := hι have hz' : ∀ j : ι, ∃ x ∈ Icc r s, (f x, fun i => g i x) = z j := by intro j rcases hz j with ⟨x, hx, hzx⟩ exact ⟨x, hx, hzx⟩ choose x hx hzx using hz' let ω : Measure ℝ := Measure.sum fun j : ι => ofReal (w j) • Measure.dirac (x j) have hp : IsProbabilityMeasure ω := by dsimp [ω] apply HasSum.isProbabilityMeasure_sum_dirac hw₀ simpa [hw₁] using (hasSum_fintype w) have hmass (A : Set ℝ) (hA : ∀ j, x j ∈ A) : ω A = 1 := by have hdirac : ∀ j, Measure.dirac (x j) A = 1 := by intro j exact Measure.dirac_apply_of_mem (hA j) change (Measure.sum fun j : ι => ofReal (w j) • Measure.dirac (x j)) A = 1 rw [Measure.sum_apply_of_countable, tsum_fintype] simp only [Measure.smul_apply, hdirac, smul_eq_mul, mul_one] rw [← ENNReal.ofReal_sum_of_nonneg (fun j _ => hw₀ j), hw₁] simp have hint (F : ℝ → ℝ) : (∫ t, F t ∂ω) = ∑ j, w j * F (x j) := by change (∫ t, F t ∂Measure.sum (fun j : ι => ofReal (w j) • Measure.dirac (x j))) = _ rw [integral_sum_dirac (by simp), tsum_fintype] apply Finset.sum_congr rfl intro j hj simp [ENNReal.toReal_ofReal (hw₀ j), smul_eq_mul] refine ⟨ω, hp, ?_, hmass _ hx, ?_, ?_⟩ · refine ⟨Finset.univ.image x, ?_⟩ apply hmass intro j simp · rw [hint] have hproj := congrArg fst hsum simpa only [Prod.fst_sum, Prod.smul_fst, ← hzx, fst, smul_eq_mul] using hproj · intro i rw [hint] have hproj := congrArg (fun z : ℝ × (Fin m → ℝ) => z.2 i) hsum simpa only [Prod.snd_sum, Prod.smul_snd, ← hzx, snd, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using hproj

theorem isCompact_matchingFiberPairs {m : ℕ} {S : Set (ℝ × (Fin m → ℝ))} (hS : IsCompact S) : IsCompact {p : (ℝ × (Fin m → ℝ)) × (ℝ × (Fin m → ℝ)) | p.1 ∈ convexHull ℝ S ∧ p.2 ∈ convexHull ℝ S ∧ p.1.2 = p.2.2} := by have hC : IsCompact (convexHull ℝ S) := isCompact_convexHull_finiteDimensional hS have hEq : IsClosed {p : (ℝ × (Fin m → ℝ)) × (ℝ × (Fin m → ℝ)) | p.1.2 = p.2.2} := isClosed_eq (by fun_prop) (by fun_prop) convert (hC.prod hC).inter_right hEq using 1 ext p simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_prod, and_assoc]

theorem tvDist_predictiveLaw_le_unmatchedTail {K : ℕ} (hK : 1 ≤ K) {b ε gap n : ℝ} (hn : 0 ≤ n) (hb : 0 ≤ b) (hε : 0 ≤ ε) (T : TriplePriors K b ε gap) : tvDist (predictiveLaw n T.ν₀) (predictiveLaw n T.ν₁) ≤ unmatchedTail K n b := by letI : IsProbabilityMeasure T.ν₀ := T.probability₀ letI : IsProbabilityMeasure T.ν₁ := T.probability₁ letI : IsProbabilityMeasure (predictiveLaw n T.ν₀) := predictiveLaw_isProbability n T.ν₀ letI : IsProbabilityMeasure (predictiveLaw n T.ν₁) := predictiveLaw_isProbability n T.ν₁ let S : Set MarkedParam := {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} have hsub : {θ : MarkedParam | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ ε ≤ θ.2.1 ∧ θ.2.1 ≤ 1 - ε ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} ⊆ S := by rintro θ ⟨hp0, hpb, hεπ, hπε, hμ0, hμ1⟩ exact ⟨hp0, hpb, hε.trans hεπ, hπε.trans (by linarith), hμ0, hμ1⟩ have hs0 : T.ν₀ S = 1 := by apply le_antisymm prob_le_one rw [← T.supported₀] exact measure_mono hsub have hs1 : T.ν₁ S = 1 := by apply le_antisymm prob_le_one rw [← T.supported₁] exact measure_mono hsub let E (ν : Measure MarkedParam) (z : (ℕ × ℕ) × ℕ) : ℝ := ∑' t : ℕ, if 3 * K < t + z.1.1 + z.1.2 + z.2 then ∫ θ, markedEnvelopeCoeff n θ t z.1.1 z.1.2 z.2 ∂ν else 0 obtain ⟨hEt0, hE0, htail0⟩ := tsum_unmatchedEnvelope_integral_le_tail hK hn hb T.ν₀ T.finite₀ hs0 obtain ⟨hEt1, hE1, htail1⟩ := tsum_unmatchedEnvelope_integral_le_tail hK hn hb T.ν₁ T.finite₁ hs1 have hpoint (z : (ℕ × ℕ) × ℕ) : |(predictiveLaw n T.ν₀).real {z} - (predictiveLaw n T.ν₁).real {z}| ≤ E T.ν₀ z + E T.ν₁ z := by rcases z with ⟨⟨u, v⟩, w⟩ calc _ ≤ ∑' t : ℕ, if 3 * K < t + u + v + w then (∫ θ, markedEnvelopeCoeff n θ t u v w ∂T.ν₀) + (∫ θ, markedEnvelopeCoeff n θ t u v w ∂T.ν₁) else 0 := abs_predictiveLaw_singleton_diff_le_unmatchedEnvelope hn hε T u v w _ = ∑' t : ℕ, ( (if 3 * K < t + u + v + w then ∫ θ, markedEnvelopeCoeff n θ t u v w ∂T.ν₀ else 0) + (if 3 * K < t + u + v + w then ∫ θ, markedEnvelopeCoeff n θ t u v w ∂T.ν₁ else 0)) := by apply tsum_congr intro t split_ifs <;> simp _ = E T.ν₀ ((u, v), w) + E T.ν₁ ((u, v), w) := by simpa only [E] using (hEt0 ((u, v), w)).tsum_add (hEt1 ((u, v), w)) have hEsum : Summable (fun z => E T.ν₀ z + E T.ν₁ z) := hE0.add hE1 have hlhs : Summable (fun z : (ℕ × ℕ) × ℕ => |(predictiveLaw n T.ν₀).real {z} - (predictiveLaw n T.ν₁).real {z}|) := by apply Summable.of_nonneg_of_le (f := fun z => E T.ν₀ z + E T.ν₁ z) · intro z positivity · exact hpoint · exact hEsum calc tvDist (predictiveLaw n T.ν₀) (predictiveLaw n T.ν₁) ≤ (∑' z : (ℕ × ℕ) × ℕ, |(predictiveLaw n T.ν₀).real {z} - (predictiveLaw n T.ν₁).real {z}|) / 2 := by simpa [div_eq_mul_inv, mul_comm] using tvDist_le_half_tsum_singleton_abs (predictiveLaw n T.ν₀) (predictiveLaw n T.ν₁) _ ≤ (∑' z : (ℕ × ℕ) × ℕ, (E T.ν₀ z + E T.ν₁ z)) / 2 := by apply div_le_div_of_nonneg_right _ (by norm_num) exact Summable.tsum_le_tsum hpoint hlhs hEsum _ = ((∑' z, E T.ν₀ z) + ∑' z, E T.ν₁ z) / 2 := by rw [hE0.tsum_add hE1] _ ≤ (unmatchedTail K n b + unmatchedTail K n b) / 2 := by gcongr _ = unmatchedTail K n b := by ring

theorem tvDist_predictiveLaw_le_factorial {K : ℕ} (hK : 1 ≤ K) {b ε gap n : ℝ} (hn : 0 ≤ n) (hb : 0 ≤ b) (hε : 0 ≤ ε) (T : TriplePriors K b ε gap) : tvDist (predictiveLaw n T.ν₀) (predictiveLaw n T.ν₁) ≤ exp (2 * n * b) * (2 * n * b) ^ (3 * K + 1) / (factorial (3 * K + 1) : ℝ) := by exact (tvDist_predictiveLaw_le_unmatchedTail hK hn hb hε T).trans (unmatchedTail_le_factorial K hn hb)

theorem tvDist_productPredictive_le_sum {d K : ℕ} (hK : 1 ≤ K) {b ε gap n : ℝ} (hn : 0 ≤ n) (hb : 0 ≤ b) (hε : 0 ≤ ε) (T : Fin d → TriplePriors K b ε gap) : tvDist (Measure.pi fun i : Fin d => predictiveLaw n (T i).ν₀) (Measure.pi fun i : Fin d => predictiveLaw n (T i).ν₁) ≤ ∑ _i : Fin d, unmatchedTail K n b := by letI : ∀ i : Fin d, IsProbabilityMeasure (predictiveLaw n (T i).ν₀) := fun i => by letI := (T i).probability₀ exact predictiveLaw_isProbability n (T i).ν₀ letI : ∀ i : Fin d, IsProbabilityMeasure (predictiveLaw n (T i).ν₁) := fun i => by letI := (T i).probability₁ exact predictiveLaw_isProbability n (T i).ν₁ calc _ ≤ ∑ i : Fin d, tvDist (predictiveLaw n (T i).ν₀) (predictiveLaw n (T i).ν₁) := tvDist_pi_le_sum_heterogeneous _ _ _ ≤ ∑ _i : Fin d, unmatchedTail K n b := by apply Finset.sum_le_sum intro i hi exact tvDist_predictiveLaw_le_unmatchedTail hK hn hb hε (T i)

theorem tsum_integral_unmatchedEnvelopeCoeff_le_tail {K : ℕ} (hK : 1 ≤ K) {n b : ℝ} (hn : 0 ≤ n) (hb : 0 ≤ b) (ν : Measure MarkedParam) [IsProbabilityMeasure ν] (hfinite : ∃ s : Finset MarkedParam, ν (s : Set MarkedParam) = 1) (hsupport : ν {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} = 1) : Summable (fun q : Fin 4 → ℕ => ∫ θ, if 3 * K < q 0 + q 1 + q 2 + q 3 then markedEnvelopeCoeff n θ (q 0) (q 1) (q 2) (q 3) else 0 ∂ν) ∧ (∑' q : Fin 4 → ℕ, ∫ θ, if 3 * K < q 0 + q 1 + q 2 + q 3 then markedEnvelopeCoeff n θ (q 0) (q 1) (q 2) (q 3) else 0 ∂ν) ≤ unmatchedTail K n b := by classical let G : Set MarkedParam := {θ | 0 ≤ θ.1 ∧ θ.1 ≤ b ∧ 0 ≤ θ.2.1 ∧ θ.2.1 ≤ 1 ∧ 0 ≤ θ.2.2 ∧ θ.2.2 ≤ 1} let F (q : Fin 4 → ℕ) (θ : MarkedParam) : ℝ := if θ ∈ G then if 3 * K < q 0 + q 1 + q 2 + q 3 then markedEnvelopeCoeff n θ (q 0) (q 1) (q 2) (q 3) else 0 else 0 have hGae : ∀ᵐ θ ∂ν, θ ∈ G := (mem_ae_iff_prob_eq_one (by measurability : MeasurableSet G)).2 hsupport have hFsum (θ : MarkedParam) : Summable (fun q => F q θ) := by by_cases hθ : θ ∈ G · exact (unmatchedEnvelopeCoeff_pointwise_le_tail hK hn θ hθ.1 hθ.2.1 hθ.2.2.1 hθ.2.2.2.1 hθ.2.2.2.2.1 hθ.2.2.2.2.2).1.congr (fun q => by simp [F, hθ]) · simp [F, hθ] have hint (q : Fin 4 → ℕ) : (∫ θ, if 3 * K < q 0 + q 1 + q 2 + q 3 then markedEnvelopeCoeff n θ (q 0) (q 1) (q 2) (q 3) else 0 ∂ν) = ∫ θ, F q θ ∂ν := by apply integral_congr_ae filter_upwards [hGae] with θ hθ simp [F, hθ] have hsum : Summable (fun q : Fin 4 → ℕ => ∫ θ, F q θ ∂ν) := finiteSupport_summable_integral ν hfinite F hFsum constructor · exact hsum.congr (fun q => (hint q).symm) · simp_rw [hint] rw [← finiteSupport_integral_tsum ν hfinite F hFsum] calc (∫ θ, ∑' q, F q θ ∂ν) ≤ ∫ _θ, unmatchedTail K n b ∂ν := by apply integral_mono_ae · exact finiteSupport_integrable ν hfinite _ · exact finiteSupport_integrable ν hfinite _ · filter_upwards with θ by_cases hθ : θ ∈ G · simpa [F, hθ] using (unmatchedEnvelopeCoeff_pointwise_le_tail hK hn θ hθ.1 hθ.2.1 hθ.2.2.1 hθ.2.2.2.1 hθ.2.2.2.2.1 hθ.2.2.2.2.2).2 · simp [F, hθ] unfold unmatchedTail exact tsum_nonneg fun m => by split_ifs <;> positivity _ = unmatchedTail K n b := by simp

theorem scalarPriors_to_triple {K : ℕ} (hK : 1 ≤ K) {a q gap b ε : ℝ} (ha₀ : 0 < a) (hq : q = 1 - 2 * ε) (hε₀ : 0 < ε) (hε₁ : ε < 1 / 2) (hb : 0 < b) (S : ScalarPriors K a q gap) : ∃ T : TriplePriors K b ε (a * b * gap), T.ν₀ = triplePrior b a q S.ω₀ ∧ T.ν₁ = triplePrior b a q S.ω₁ ∧ (∫ t, t.1 ∂T.ν₀) = a * b := by have hq₀ : 0 ≤ q := by rw [hq]; linarith have hq₁ : q ≤ 1 := by rw [hq]; linarith have hpolyInt (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) (n j : ℕ) : Integrable (fun x : ℝ => x ^ n * (x + q * a) ^ j) ω := by have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := ae_iff.mpr ((prob_compl_eq_zero_iff measurableSet_Icc).2 hs) have hc : ContinuousOn (fun x : ℝ => x ^ n * (x + q * a) ^ j) (Icc a 1) := by fun_prop have hi := hc.integrableOn_compact isCompact_Icc (μ := ω) have hu : (Set.univ : Set ℝ) =ᵐ[ω] Icc a 1 := by filter_upwards [hae] with x hx exact propext (iff_of_true trivial hx) simpa using hi.congr_set_ae hu have hinvInt (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) (j : ℕ) : Integrable (fun x : ℝ => x⁻¹ * (x + q * a) ^ j) ω := by have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := ae_iff.mpr ((prob_compl_eq_zero_iff measurableSet_Icc).2 hs) have hc : ContinuousOn (fun x : ℝ => x⁻¹ * (x + q * a) ^ j) (Icc a 1) := by apply ContinuousOn.mul · apply continuousOn_id.inv₀ intro x hx exact ne_of_gt (lt_of_lt_of_le ha₀ hx.1) · fun_prop have hi := hc.integrableOn_compact isCompact_Icc (μ := ω) have hu : (Set.univ : Set ℝ) =ᵐ[ω] Icc a 1 := by filter_upwards [hae] with x hx exact propext (iff_of_true trivial hx) simpa using hi.congr_set_ae hu have hpoly : ∀ n j : ℕ, n + j ≤ 3 * K → (∫ x, x ^ n * (x + q * a) ^ j ∂S.ω₀) = ∫ x, x ^ n * (x + q * a) ^ j ∂S.ω₁ := by intro n j induction j generalizing n with | zero => intro hn simpa using S.ordinary_match n (by simpa using hn) | succ j ih => intro hn letI := S.probability₀ letI := S.probability₁ have h₁ := ih (n + 1) (by omega) have h₂ := ih n (by omega) have hpoint (x : ℝ) : x ^ n * (x + q * a) ^ (j + 1) = x ^ (n + 1) * (x + q * a) ^ j + q * a * (x ^ n * (x + q * a) ^ j) := by rw [pow_succ, pow_succ] ring have hsplit (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) : (∫ x, x ^ n * (x + q * a) ^ (j + 1) ∂ω) = (∫ x, x ^ (n + 1) * (x + q * a) ^ j ∂ω) + q * a * (∫ x, x ^ n * (x + q * a) ^ j ∂ω) := by simp_rw [hpoint] rw [integral_add (hpolyInt ω hs (n + 1) j) ((hpolyInt ω hs n j).const_mul (q * a)), integral_const_mul] rw [hsplit S.ω₀ S.supported₀, hsplit S.ω₁ S.supported₁, h₁, h₂] have hinv : ∀ j : ℕ, j ≤ 3 * K → (∫ x, x⁻¹ * (x + q * a) ^ j ∂S.ω₀) = ∫ x, x⁻¹ * (x + q * a) ^ j ∂S.ω₁ := by intro j induction j with | zero => intro _ simpa using S.inverse_match | succ j ih => intro hj letI := S.probability₀ letI := S.probability₁ have h₁ := hpoly 0 j (by omega) have h₂ := ih (by omega) have hpoint (x : ℝ) (hx : x ∈ Icc a 1) : x⁻¹ * (x + q * a) ^ (j + 1) = (x + q * a) ^ j + q * a * (x⁻¹ * (x + q * a) ^ j) := by have hxne : x ≠ 0 := ne_of_gt (lt_of_lt_of_le ha₀ hx.1) rw [pow_succ] field_simp have hsplit (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) : (∫ x, x⁻¹ * (x + q * a) ^ (j + 1) ∂ω) = (∫ x, (x + q * a) ^ j ∂ω) + q * a * (∫ x, x⁻¹ * (x + q * a) ^ j ∂ω) := by have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := ae_iff.mpr ((prob_compl_eq_zero_iff measurableSet_Icc).2 hs) calc _ = ∫ x, (x + q * a) ^ j + q * a * (x⁻¹ * (x + q * a) ^ j) ∂ω := integral_congr_ae (hae.mono fun x hx => hpoint x hx) _ = _ := by rw [integral_add (by simpa using hpolyInt ω hs 0 j) ((hinvInt ω hs j).const_mul (q * a)), integral_const_mul] rw [hsplit S.ω₀ S.supported₀, hsplit S.ω₁ S.supported₁] simpa using congrArg₂ (fun u v : ℝ => u + q * a * v) h₁ h₂ have hmixed (i j k : ℕ) (hdeg : i + j + k ≤ 3 * K) : (∫ t, mixedMonomial i j k t ∂triplePrior b a q S.ω₀) = ∫ t, mixedMonomial i j k t ∂triplePrior b a q S.ω₁ := by letI := S.probability₀ letI := S.probability₁ by_cases hz : i + j + k = 0 · have hi : i = 0 := by omega have hj : j = 0 := by omega have hk : k = 0 := by omega subst i; subst j; subst k have hp₀ := (reweightedScalar_probability_finite_supported ha₀ S.ω₀ S.finite₀ S.supported₀).1 have hp₁ := (reweightedScalar_probability_finite_supported ha₀ S.ω₁ S.finite₁ S.supported₁).1 have hmap : Measurable (scalarToTriple b a q) := by unfold scalarToTriple apply Measurable.ite (measurableSet_singleton 0) · fun_prop · fun_prop haveI : IsProbabilityMeasure (triplePrior b a q S.ω₀) := by exact (Measure.isProbabilityMeasure_map_iff hmap.aemeasurable).2 hp₀ haveI : IsProbabilityMeasure (triplePrior b a q S.ω₁) := by exact (Measure.isProbabilityMeasure_map_iff hmap.aemeasurable).2 hp₁ simp [mixedMonomial] · have hpos : 0 < i + j + k := Nat.pos_of_ne_zero hz rw [integral_mixedMonomial_triplePrior ha₀ hq₀ S.ω₀ S.supported₀ i j k hpos, integral_mixedMonomial_triplePrior ha₀ hq₀ S.ω₁ S.supported₁ i j k hpos] by_cases hn : i + k = 0 · have hi : i = 0 := by omega have hk : k = 0 := by omega subst i; subst k have hscalar (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) : (∫ x, a * b ^ (0 + j + 0) / (2 : ℝ) ^ (j + 0) * x ^ (0 + 0) / x * (x + q * a) ^ j ∂ω) = a * b ^ j / (2 : ℝ) ^ j * (∫ x, x⁻¹ * (x + q * a) ^ j ∂ω) := by have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := ae_iff.mpr ((prob_compl_eq_zero_iff measurableSet_Icc).2 hs) calc _ = ∫ x, (a * b ^ j / (2 : ℝ) ^ j) * (x⁻¹ * (x + q * a) ^ j) ∂ω := by congr 1; funext x; simp [div_eq_mul_inv]; ring _ = _ := integral_const_mul .. rw [hscalar S.ω₀ S.supported₀, hscalar S.ω₁ S.supported₁, hinv j (by omega)] · have hnpos : 0 < i + k := Nat.pos_of_ne_zero hn let n := i + k - 1 have hbound : n + j ≤ 3 * K := by dsimp [n]; omega have hscalar (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) : (∫ x, a * b ^ (i + j + k) / (2 : ℝ) ^ (j + k) * x ^ (i + k) / x * (x + q * a) ^ j ∂ω) = (a * b ^ (i + j + k) / (2 : ℝ) ^ (j + k)) * (∫ x, x ^ n * (x + q * a) ^ j ∂ω) := by have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := ae_iff.mpr ((prob_compl_eq_zero_iff measurableSet_Icc).2 hs) calc _ = ∫ x, (a * b ^ (i + j + k) / (2 : ℝ) ^ (j + k)) * (x ^ n * (x + q * a) ^ j) ∂ω := by apply integral_congr_ae filter_upwards [hae] with x hx have hxne : x ≠ 0 := ne_of_gt (lt_of_lt_of_le ha₀ hx.1) have he : i + k = n + 1 := by dsimp [n]; omega have hpow : x ^ (i + k) / x = x ^ n := by rw [he, pow_succ] field_simp calc _ = (a * b ^ (i + j + k) / (2 : ℝ) ^ (j + k)) * ((x ^ (i + k) / x) * (x + q * a) ^ j) := by ring _ = _ := by rw [hpow] _ = _ := integral_const_mul .. rw [hscalar S.ω₀ S.supported₀, hscalar S.ω₁ S.supported₁, hpoly n j hbound] have hmap : Measurable (scalarToTriple b a q) := by unfold scalarToTriple apply Measurable.ite (measurableSet_singleton 0) · fun_prop · fun_prop let A : Set MarkedParam := {t | 0 ≤ t.1 ∧ t.1 ≤ b ∧ ε ≤ t.2.1 ∧ t.2.1 ≤ 1 - ε ∧ 0 ≤ t.2.2 ∧ t.2.2 ≤ 1} have hA : MeasurableSet A := by dsimp [A]; measurability have hpoint (x : ℝ) (hx : x ∈ ({0} ∪ Icc a 1)) : scalarToTriple b a q x ∈ A := by rcases hx with hx | hx · have hx0 : x = 0 := hx subst x dsimp [A, scalarToTriple] simp constructor · exact le_of_lt hb constructor · linarith · linarith · have hxpos : 0 < x := lt_of_lt_of_le ha₀ hx.1 have hxne : x ≠ 0 := ne_of_gt hxpos have hqa : 0 ≤ q * a := mul_nonneg hq₀ ha₀.le have hden : 0 < x + q * a := by positivity have hratio₀ : 0 ≤ q * a / x := div_nonneg hqa hxpos.le have hratio₁ : q * a / x ≤ q := by apply (div_le_iff₀ hxpos).2 nlinarith [mul_nonneg hq₀ (sub_nonneg.mpr hx.1)] have hp₀ : 0 ≤ b * x := mul_nonneg hb.le hxpos.le have hp₁ : b * x ≤ b := by nlinarith [mul_nonneg hb.le (sub_nonneg.mpr hx.2)] have hμ₀ : 0 ≤ x / (x + q * a) := div_nonneg hxpos.le hden.le have hμ₁ : x / (x + q * a) ≤ 1 := (div_le_one hden).2 (by linarith) dsimp [A, scalarToTriple] simp only [if_neg hxne, Set.mem_setOf_eq] refine ⟨hp₀, hp₁, ?_, ?_, hμ₀, hμ₁⟩ · linarith · linarith have hcert (ω : Measure ℝ) [IsProbabilityMeasure ω] (hfin : ∃ s : Finset ℝ, ω (s : Set ℝ) = 1) (hs : ω (Icc a 1) = 1) : IsProbabilityMeasure (triplePrior b a q ω) ∧ (∃ s : Finset MarkedParam, (triplePrior b a q ω) (s : Set MarkedParam) = 1) ∧ (triplePrior b a q ω) A = 1 := by obtain ⟨hp, hfin', hs'⟩ := reweightedScalar_probability_finite_supported ha₀ ω hfin hs letI := hp have htp : IsProbabilityMeasure (triplePrior b a q ω) := by exact (Measure.isProbabilityMeasure_map_iff hmap.aemeasurable).2 hp letI := htp refine ⟨htp, ?_, ?_⟩ · obtain ⟨s, hs⟩ := hfin' refine ⟨s.image (scalarToTriple b a q), ?_⟩ rw [triplePrior, Measure.map_apply hmap (Finset.measurableSet _)] apply le_antisymm prob_le_one calc 1 = (reweightedScalar a ω) (s : Set ℝ) := hs.symm _ ≤ (reweightedScalar a ω) ((scalarToTriple b a q) ⁻¹' (s.image (scalarToTriple b a q) : Set MarkedParam)) := measure_mono (by intro x hx; exact Finset.mem_image.mpr ⟨x, hx, rfl⟩) · rw [triplePrior, Measure.map_apply hmap hA] apply le_antisymm prob_le_one calc 1 = (reweightedScalar a ω) ({0} ∪ Icc a 1) := hs'.symm _ ≤ (reweightedScalar a ω) ((scalarToTriple b a q) ⁻¹' A) := measure_mono (by intro x hx; exact hpoint x hx) have hmean (ω : Measure ℝ) [IsProbabilityMeasure ω] (hs : ω (Icc a 1) = 1) : (∫ t, t.1 ∂triplePrior b a q ω) = a * b := by have hmix := integral_mixedMonomial_triplePrior (b := b) ha₀ hq₀ ω hs 1 0 0 (by norm_num) have hae : ∀ᵐ x ∂ω, x ∈ Icc a 1 := ae_iff.mpr ((prob_compl_eq_zero_iff measurableSet_Icc).2 hs) -- … truncated; follow the source link for the rest …