Stat.Finite­Rao­Blackwell.Poisson.Independent­Prefix.Random­Scale­Transfer

theorem measurableSet_retentionSuccessSet (n m : ℕ) : MeasurableSet (retentionSuccessSet (X := X) (Y := Y) n m) := by exact (measurableSet_le measurable_const (measurable_finiteSample_count.comp measurable_fst)).inter (measurableSet_le measurable_const (measurable_finiteSample_count.comp measurable_snd))

theorem measurableSet_retentionFailureSet (n m : ℕ) : MeasurableSet (retentionFailureSet (X := X) (Y := Y) n m) := by exact (measurableSet_lt (measurable_finiteSample_count.comp measurable_fst) measurable_const).union (measurableSet_lt (measurable_finiteSample_count.comp measurable_snd) measurable_const)

theorem retentionSuccessSet_eq_compl_failureSet (n m : ℕ) : retentionSuccessSet (X := X) (Y := Y) n m = (retentionFailureSet (X := X) (Y := Y) n m)ᶜ := by ext z simp [retentionSuccessSet, retentionFailureSet]

theorem measurable_orderedPrefix (fallback : Fin n → X) : Measurable (orderedPrefix fallback : FiniteSample X → (Fin n → X)) := by unfold orderedPrefix apply measurable_pi_lambda intro i t ht rw [MeasurableSpace.measurableSet_iInf] intro k change MeasurableSet ((fun x : Fin k → X => (if h : n ≤ k then fun i => x (castLE h i) else fallback) i) ⁻¹' t) by_cases h : n ≤ k · simp only [dif_pos h] exact ht.preimage (measurable_pi_apply (castLE h i)) · simp only [dif_neg h] exact measurable_const ht

theorem measurable_twoPoolOrderedRetention (fallbackX : Fin n → X) (fallbackY : Fin m → Y) : Measurable (twoPoolOrderedRetention fallbackX fallbackY) := by exact (measurable_orderedPrefix fallbackX).comp measurable_fst |>.prodMk ((measurable_orderedPrefix fallbackY).comp measurable_snd)

theorem map_orderedPrefix_restrict_count_ge (P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) (fallback : Fin n → X) : Measure.map (orderedPrefix fallback) ((finitePoissonSampleLaw P lambda).restrict (FiniteSample.count ⁻¹' Set.Ici n)) = (poissonMeasure lambda) (Set.Ici n) • Measure.pi (fun _ : Fin n => P) := by let μ := finitePoissonSampleLaw P lambda have hdecomp : μ.restrict (FiniteSample.count ⁻¹' Set.Ici n) = Measure.sum (fun k : (Set.Ici n : Set ℕ) => μ.restrict (FiniteSample.count ⁻¹' ({k.1} : Set ℕ))) := by rw [← Set.biUnion_preimage_singleton] exact Measure.restrict_biUnion (Set.to_countable (Set.Ici n)) (pairwiseDisjoint_fiber FiniteSample.count (Set.Ici n)) (fun k => measurable_finiteSample_count (measurableSet_singleton k)) rw [show finitePoissonSampleLaw P lambda = μ by rfl, hdecomp, Measure.map_sum ((measurable_orderedPrefix fallback).aemeasurable)] simp_rw [show ∀ k : (Set.Ici n : Set ℕ), Measure.map (orderedPrefix fallback) (μ.restrict (FiniteSample.count ⁻¹' ({k.1} : Set ℕ))) = (poissonMeasure lambda) ({k.1} : Set ℕ) • Measure.pi (fun _ : Fin n => P) by intro k rw [show μ = finitePoissonSampleLaw P lambda by rfl, finitePoissonSampleLaw_restrict_count_eq, Measure.map_smul, map_orderedPrefix_fixedSizeEmbed_pi P fallback k.2]] ext A hA simp only [Measure.sum_apply _ hA, Measure.smul_apply, smul_eq_mul] rw [ENNReal.tsum_mul_right] congr 1 simpa using (tsum_measure_preimage_singleton (μ := poissonMeasure lambda) (s := Set.Ici n) (f := id) (Set.to_countable (Set.Ici n)) (fun k _ => measurableSet_singleton k))

theorem normalized_map_twoPoolOrderedRetention_restrict_success (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lambdaX lambdaY : ℝ≥0) (n m : ℕ) (fallbackX : Fin n → X) (fallbackY : Fin m → Y) (hpos : (poissonMeasure lambdaX) (Ici n) * (poissonMeasure lambdaY) (Ici m) ≠ 0) : (((poissonMeasure lambdaX) (Ici n) * (poissonMeasure lambdaY) (Ici m))⁻¹) • Measure.map (twoPoolOrderedRetention fallbackX fallbackY) (((finitePoissonSampleLaw P lambdaX).prod (finitePoissonSampleLaw Q lambdaY)).restrict (retentionSuccessSet (X := X) (Y := Y) n m)) = fixedPoolsLaw P Q n m := by rw [map_twoPoolOrderedRetention_restrict_success] rw [smul_smul, ENNReal.inv_mul_cancel hpos (ENNReal.mul_ne_top (measure_ne_top _ _) (measure_ne_top _ _)), one_smul]

theorem map_orderedPrefix_rawMixture (pi : Measure Theta) (P : Kernel Theta X) [∀ theta, IsProbabilityMeasure (P theta)] (S : Theta → ℝ≥0) (u : ℝ≥0) {n : ℕ} (fallback : Fin n → X) (hraw : AEMeasurable (fun theta => finitePoissonSampleLaw (P theta) (u * S theta)) pi) : Measure.map (orderedPrefix fallback) (rawMixture pi P S u) = pi.bind (fun theta => Measure.map (orderedPrefix fallback) (finitePoissonSampleLaw (P theta) (u * S theta))) := by unfold rawMixture Measure.bind rw [← Measure.join_map_map (measurable_orderedPrefix fallback), (Measure.measurable_map _ (measurable_orderedPrefix fallback)).aemeasurable |>.map_map_of_aemeasurable hraw] rfl

theorem tvDist_fixedMixture_map_rawMixture_le (pi : Measure Theta) [IsProbabilityMeasure pi] (P : Kernel Theta X) [∀ theta, IsProbabilityMeasure (P theta)] (S : Theta → ℝ≥0) (u : ℝ≥0) (n : ℕ) (fallback : Fin n → X) (hfixed : AEMeasurable (fun theta => Measure.pi (fun _ : Fin n => P theta)) pi) (hraw : AEMeasurable (fun theta => finitePoissonSampleLaw (P theta) (u * S theta)) pi) : tvDist (fixedMixture pi P n) (Measure.map (orderedPrefix fallback) (rawMixture pi P S u)) ≤ ∫ theta, (poissonMeasure (u * S theta) (Set.Iio n)).toReal ∂pi := by have hf := measurable_orderedPrefix fallback let bad : Set (FiniteSample X) := FiniteSample.count ⁻¹' Set.Iio n have hbad : MeasurableSet bad := (by measurability : MeasurableSet (Set.Iio n)).preimage measurable_finiteSample_count have hcount (theta : Theta) : finitePoissonSampleLaw (P theta) (u * S theta) bad = poissonMeasure (u * S theta) (Set.Iio n) := by rw [← finitePoissonSampleLaw_map_count (P theta) (u * S theta), Measure.map_apply measurable_finiteSample_count (by measurability)] have hfailure : AEMeasurable (fun theta => poissonMeasure (u * S theta) (Set.Iio n)) pi := by simpa only [Function.comp_def, hcount] using (Measure.measurable_coe hbad).comp_aemeasurable hraw have ifailure : Integrable (fun theta => (poissonMeasure (u * S theta) (Set.Iio n)).toReal) pi := by apply (integrable_const (1 : ℝ)).mono' hfailure.ennreal_toReal.aestronglyMeasurable exact Filter.Eventually.of_forall fun theta => by rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] exact measureReal_le_one unfold tvDist apply ciSup_le rintro ⟨A, hA⟩ let B := orderedPrefix fallback ⁻¹' A have hB : MeasurableSet B := hA.preimage hf have hmfixed := (Measure.measurable_coe hA).comp_aemeasurable hfixed have hmraw := (Measure.measurable_coe hB).comp_aemeasurable hraw have ifixed : Integrable (fun theta => (Measure.pi (fun _ : Fin n => P theta)).real A) pi := by apply (integrable_const (1 : ℝ)).mono' hmfixed.ennreal_toReal.aestronglyMeasurable exact Filter.Eventually.of_forall fun theta => by rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] exact measureReal_le_one have iraw : Integrable (fun theta => (finitePoissonSampleLaw (P theta) (u * S theta)).real B) pi := by apply (integrable_const (1 : ℝ)).mono' hmraw.ennreal_toReal.aestronglyMeasurable exact Filter.Eventually.of_forall fun theta => by rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg] exact measureReal_le_one have efixed : (fixedMixture pi P n).real A = ∫ theta, (Measure.pi (fun _ : Fin n => P theta)).real A ∂pi := by rw [fixedMixture, measureReal_def, Measure.bind_apply hA hfixed] exact (integral_toReal hmfixed (Filter.Eventually.of_forall fun theta => measure_lt_top _ _)).symm have eraw : (Measure.map (orderedPrefix fallback) (rawMixture pi P S u)).real A = ∫ theta, (finitePoissonSampleLaw (P theta) (u * S theta)).real B ∂pi := by rw [map_measureReal_apply hf hA, rawMixture, measureReal_def, Measure.bind_apply hB hraw] exact (integral_toReal hmraw (Filter.Eventually.of_forall fun theta => measure_lt_top _ _)).symm change |(fixedMixture pi P n).real A - (Measure.map (orderedPrefix fallback) (rawMixture pi P S u)).real A| ≤ _ rw [efixed, eraw, ← integral_sub ifixed iraw] refine (abs_integral_le_integral_abs).trans (integral_mono (ifixed.sub iraw).abs ifailure ?_) intro theta let : IsProbabilityMeasure (Measure.map (orderedPrefix fallback) (finitePoissonSampleLaw (P theta) (u * S theta))) := Measure.isProbabilityMeasure_map hf.aemeasurable change |(Measure.pi (fun _ : Fin n => P theta)).real A - (finitePoissonSampleLaw (P theta) (u * S theta)).real B| ≤ (poissonMeasure (u * S theta) (Set.Iio n)).toReal rw [show (finitePoissonSampleLaw (P theta) (u * S theta)).real B = (Measure.map (orderedPrefix fallback) (finitePoissonSampleLaw (P theta) (u * S theta))).real A from (map_measureReal_apply hf hA).symm] exact (abs_measureReal_sub_le_tvDist hA).trans (tvDist_iid_map_orderedPrefix_le (P theta) (u * S theta) fallback)

theorem measurable_transferredRawRule (n m : ℕ) {rule : FixedPools (X := X) (Y := Y) n m → A} (hrule : Measurable rule) (fallbackX : Fin n → X) (fallbackY : Fin m → Y) (fallbackA : A) : Measurable (transferredRawRule n m rule fallbackX fallbackY fallbackA) := by unfold transferredRawRule exact Measurable.ite (measurableSet_retentionSuccessSet n m) (hrule.comp (measurable_twoPoolOrderedRetention fallbackX fallbackY)) measurable_const

theorem measurable_decisionRisk {Z : Type uZ} [MeasurableSpace Z] (K : Kernel Theta Z) [IsSFiniteKernel K] {loss : Theta → A → ℝ≥0∞} (hloss : Measurable (uncurry loss)) {rule : Z → A} (hrule : Measurable rule) : Measurable (decisionRisk K loss rule) := by /- Apply `Measurable.lintegral_kernel_prod_right` to the jointly measurable integrand `(theta, z) ↦ loss theta (rule z)`. The s-finiteness assumption is essential for the parameterized-integral theorem and is automatic for the probability kernels used below. -/ unfold decisionRisk apply Measurable.lintegral_kernel_prod_right (κ := K) (f := fun theta z => loss theta (rule z)) exact hloss.comp (measurable_fst.prodMk (hrule.comp measurable_snd))

theorem bayesDecisionRisk_transferredRawRule_le (pi : Measure Theta) [IsProbabilityMeasure pi] (Kraw : Kernel Theta (RawTwoPool X Y)) (Kfixed : Kernel Theta (FixedPools (X := X) (Y := Y) n m)) (P : Kernel Theta X) (Q : Kernel Theta Y) [∀ theta, IsProbabilityMeasure (P theta)] [∀ theta, IsProbabilityMeasure (Q theta)] (S : Theta → ℝ≥0) (u v : ℝ≥0) (hraw : IsRandomScaleTwoPoolExperiment Kraw P Q S u v) (hfixed : IsFixedTwoPoolExperiment n m Kfixed P Q) (loss : Theta → A → ℝ≥0∞) (B : ℝ≥0∞) (hB : B ≠ ⊤) (hloss : Measurable (uncurry loss)) (hbound : ∀ theta a, loss theta a ≤ B) (rule : FixedPools (X := X) (Y := Y) n m → A) (hrule : Measurable rule) (fallbackX : Fin n → X) (fallbackY : Fin m → Y) (fallbackA : A) : bayesDecisionRisk pi Kraw loss (transferredRawRule n m rule fallbackX fallbackY fallbackA) ≤ bayesDecisionRisk pi Kfixed loss rule + B * priorPredictive pi Kraw (retentionFailureSet (X := X) (Y := Y) n m) := by /- Integrate `decisionRisk_transferredRawRule_le` over the prior. Use `lintegral_add_left`, `lintegral_const_mul`, and `priorPredictive_apply` to identify the integrated conditional failure probability. -/ letI : IsMarkovKernel Kraw := ⟨fun theta => by rw [hraw theta] infer_instance⟩ letI : IsMarkovKernel Kfixed := ⟨fun theta => by rw [hfixed theta] unfold fixedPoolsLaw infer_instance⟩ have hfixedRisk : Measurable (decisionRisk Kfixed loss rule) := by unfold decisionRisk apply Measurable.lintegral_kernel_prod_right (κ := Kfixed) (f := fun theta z => loss theta (rule z)) exact hloss.comp (measurable_fst.prodMk (hrule.comp measurable_snd)) unfold bayesDecisionRisk calc (∫⁻ theta, decisionRisk Kraw loss (transferredRawRule n m rule fallbackX fallbackY fallbackA) theta ∂pi) ≤ ∫⁻ theta, decisionRisk Kfixed loss rule theta + B * Kraw theta (retentionFailureSet (X := X) (Y := Y) n m) ∂pi := by apply lintegral_mono intro theta exact decisionRisk_transferredRawRule_le Kraw Kfixed P Q S u v hraw hfixed loss B hB hloss hbound rule hrule fallbackX fallbackY fallbackA theta _ = (∫⁻ theta, decisionRisk Kfixed loss rule theta ∂pi) + ∫⁻ theta, B * Kraw theta (retentionFailureSet (X := X) (Y := Y) n m) ∂pi := by rw [lintegral_add_left hfixedRisk] _ = (∫⁻ theta, decisionRisk Kfixed loss rule theta ∂pi) + B * ∫⁻ theta, Kraw theta (retentionFailureSet (X := X) (Y := Y) n m) ∂pi := by rw [lintegral_const_mul] exact Kraw.measurable_coe (measurableSet_retentionFailureSet n m) _ = (∫⁻ theta, decisionRisk Kfixed loss rule theta ∂pi) + B * priorPredictive pi Kraw (retentionFailureSet (X := X) (Y := Y) n m) := by rw [priorPredictive_apply pi Kraw (measurableSet_retentionFailureSet n m)]

theorem bayesDecisionRisk_le_worstCase (pi : Measure Theta) [IsProbabilityMeasure pi] {Z : Type uZ} [MeasurableSpace Z] (K : Kernel Theta Z) (loss : Theta → A → ℝ≥0∞) (rule : Z → A) : bayesDecisionRisk pi K loss rule ≤ worstCaseDecisionRisk K loss rule := by unfold bayesDecisionRisk worstCaseDecisionRisk apply lintegral_le_const filter_upwards with theta exact le_iSup (fun theta => decisionRisk K loss rule theta) theta

theorem bayesDecisionRisk_transferredRawRule_le_worstCase_add (pi : Measure Theta) [IsProbabilityMeasure pi] (Kraw : Kernel Theta (RawTwoPool X Y)) (Kfixed : Kernel Theta (FixedPools (X := X) (Y := Y) n m)) (P : Kernel Theta X) (Q : Kernel Theta Y) [∀ theta, IsProbabilityMeasure (P theta)] [∀ theta, IsProbabilityMeasure (Q theta)] (S : Theta → ℝ≥0) (u v : ℝ≥0) (hraw : IsRandomScaleTwoPoolExperiment Kraw P Q S u v) (hfixed : IsFixedTwoPoolExperiment n m Kfixed P Q) (loss : Theta → A → ℝ≥0∞) (B eps : ℝ≥0∞) (hB : B ≠ ⊤) (hloss : Measurable (uncurry loss)) (hbound : ∀ theta a, loss theta a ≤ B) (hfail : priorPredictive pi Kraw (retentionFailureSet (X := X) (Y := Y) n m) ≤ eps) (rule : FixedPools (X := X) (Y := Y) n m → A) (hrule : Measurable rule) (fallbackX : Fin n → X) (fallbackY : Fin m → Y) (fallbackA : A) : bayesDecisionRisk pi Kraw loss (transferredRawRule n m rule fallbackX fallbackY fallbackA) ≤ worstCaseDecisionRisk Kfixed loss rule + B * eps := by /- Chain `bayesDecisionRisk_transferredRawRule_le`, `bayesDecisionRisk_le_worstCase`, and multiplication monotonicity applied to `hfail`. -/ exact (bayesDecisionRisk_transferredRawRule_le pi Kraw Kfixed P Q S u v hraw hfixed loss B hB hloss hbound rule hrule fallbackX fallbackY fallbackA).trans (add_le_add (bayesDecisionRisk_le_worstCase pi Kfixed loss rule) (mul_le_mul (le_refl B) hfail (by positivity) (by positivity)))

lemma randomScale_count_mixture_reconstruction {Θ X : Type*} [Fintype Θ] [MeasurableSpace Θ] [MeasurableSingletonClass Θ] [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] (π : Measure Θ) (P : Kernel Θ X) [∀ θ, IsProbabilityMeasure (P θ)] (S : Θ → ℝ≥0) (u : ℝ≥0) : histogramReconstructionKernel X ∘ₘ π.bind (fun θ => independentPoissonCountLaw (P θ) (u * S θ)) = rawMixture π P S u := by change (π.bind (fun θ => independentPoissonCountLaw (P θ) (u * S θ))).bind (histogramReconstructionKernel X) = _ rw [Measure.bind_bind (measurable_of_finite _).aemeasurable (histogramReconstructionKernel X).aemeasurable] simp_rw [show ∀ θ, (independentPoissonCountLaw (P θ) (u * S θ)).bind (histogramReconstructionKernel X) = finitePoissonSampleLaw (P θ) (u * S θ) from fun θ => independentPoissonCountLaw_comp_reconstruction (P θ) (u * S θ)] rfl

lemma randomScale_ordered_tv_le_count_tv {Θ X : Type*} [Fintype Θ] [MeasurableSpace Θ] [MeasurableSingletonClass Θ] [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] (π : Measure Θ) [IsProbabilityMeasure π] (P₀ P₁ : Kernel Θ X) [∀ θ, IsProbabilityMeasure (P₀ θ)] [∀ θ, IsProbabilityMeasure (P₁ θ)] (S : Θ → ℝ≥0) (u : ℝ≥0) : tvDist (rawMixture π P₀ S u) (rawMixture π P₁ S u) ≤ tvDist (π.bind (fun θ => independentPoissonCountLaw (P₀ θ) (u * S θ))) (π.bind (fun θ => independentPoissonCountLaw (P₁ θ) (u * S θ))) := by letI : IsProbabilityMeasure (π.bind (fun θ => independentPoissonCountLaw (P₀ θ) (u * S θ))) := isProbabilityMeasure_bind (measurable_of_finite _).aemeasurable (Filter.Eventually.of_forall fun _ => inferInstance) letI : IsProbabilityMeasure (π.bind (fun θ => independentPoissonCountLaw (P₁ θ) (u * S θ))) := isProbabilityMeasure_bind (measurable_of_finite _).aemeasurable (Filter.Eventually.of_forall fun _ => inferInstance) rw [← randomScale_count_mixture_reconstruction π P₀ S u, ← randomScale_count_mixture_reconstruction π P₁ S u] exact tvDist_bind_le _ _ (histogramReconstructionKernel X)

lemma randomScale_fixed_tv_le_count_tv_add_tail {Θ X : Type*} [Fintype Θ] [MeasurableSpace Θ] [MeasurableSingletonClass Θ] [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] (π : Measure Θ) [IsProbabilityMeasure π] (P₀ P₁ : Kernel Θ X) [∀ θ, IsProbabilityMeasure (P₀ θ)] [∀ θ, IsProbabilityMeasure (P₁ θ)] (S : Θ → ℝ≥0) (u : ℝ≥0) (n : ℕ) (fallback : Fin n → X) : tvDist (fixedMixture π P₀ n) (fixedMixture π P₁ n) ≤ tvDist (π.bind (fun θ => independentPoissonCountLaw (P₀ θ) (u * S θ))) (π.bind (fun θ => independentPoissonCountLaw (P₁ θ) (u * S θ))) + 2 * ∫ θ, (poissonMeasure (u * S θ) (Iio n)).toReal ∂π := by have ht := fixedMixture_tv_le_randomScalePoisson π P₀ P₁ S (measurable_of_finite _) u n fallback (measurable_of_finite _).aemeasurable (measurable_of_finite _).aemeasurable (measurable_of_finite _).aemeasurable (measurable_of_finite _).aemeasurable exact ht.trans (add_le_add (randomScale_ordered_tv_le_count_tv π P₀ P₁ S u) le_rfl)

theorem conditional_retentionFailure_le_poissonLowerTails (K : Kernel Theta (RawTwoPool X Y)) (P : Kernel Theta X) (Q : Kernel Theta Y) [∀ theta, IsProbabilityMeasure (P theta)] [∀ theta, IsProbabilityMeasure (Q theta)] (S : Theta → ℝ≥0) (u v : ℝ≥0) (hraw : IsRandomScaleTwoPoolExperiment K P Q S u v) (n m : ℕ) (theta : Theta) : K theta (retentionFailureSet (X := X) (Y := Y) n m) ≤ (poissonMeasure (u * S theta)) (Iio n) + (poissonMeasure (v * S theta)) (Iio m) := by /- Rewrite the raw fibre with `hraw`; express failure as the union of the two marginal count events; apply the measure union bound and `finitePoissonSampleLaw_map_count` to identify both marginals. -/ rw [hraw theta] let muX := finitePoissonSampleLaw (P theta) (u * S theta) let muY := finitePoissonSampleLaw (Q theta) (v * S theta) let AX : Set (FiniteSample X) := {s | s.count < n} let AY : Set (FiniteSample Y) := {s | s.count < m} have hfailure : retentionFailureSet (X := X) (Y := Y) n m = (AX ×ˢ univ) ∪ (univ ×ˢ AY) := by ext z simp [retentionFailureSet, AX, AY] have hcountX : muX AX = (poissonMeasure (u * S theta)) (Iio n) := by rw [← finitePoissonSampleLaw_map_count (P theta) (u * S theta), Measure.map_apply measurable_finiteSample_count measurableSet_Iio] rfl have hcountY : muY AY = (poissonMeasure (v * S theta)) (Iio m) := by rw [← finitePoissonSampleLaw_map_count (Q theta) (v * S theta), Measure.map_apply measurable_finiteSample_count measurableSet_Iio] rfl rw [hfailure] refine (measure_union_le _ _).trans ?_ rw [Measure.prod_prod, Measure.prod_prod, measure_univ, measure_univ, mul_one, one_mul, hcountX, hcountY]

theorem priorPredictive_retentionFailure_le_scaleFloor_add_integratedTails (pi : Measure Theta) [IsProbabilityMeasure pi] (K : Kernel Theta (RawTwoPool X Y)) (P : Kernel Theta X) (Q : Kernel Theta Y) [∀ theta, IsProbabilityMeasure (P theta)] [∀ theta, IsProbabilityMeasure (Q theta)] (S : Theta → ℝ≥0) (hS : Measurable S) (u v s0 : ℝ≥0) (hraw : IsRandomScaleTwoPoolExperiment K P Q S u v) (n m : ℕ) : priorPredictive pi K (retentionFailureSet (X := X) (Y := Y) n m) ≤ pi {theta | S theta < s0} + ∫⁻ theta in {theta | s0 ≤ S theta}, ((poissonMeasure (u * S theta)) (Iio n) + (poissonMeasure (v * S theta)) (Iio m)) ∂pi := by /- Expand `priorPredictive_apply`, split the parameter integral over the measurable scale event and its complement, bound the low-scale integrand by one, and use `conditional_retentionFailure_le_poissonLowerTails` on the high-scale part. -/ let A : Set Theta := {theta | S theta < s0} have hA : MeasurableSet A := measurableSet_lt hS measurable_const have hAc : Aᶜ = {theta | s0 ≤ S theta} := by ext theta simp [A] rw [priorPredictive_apply pi K (measurableSet_retentionFailureSet n m), ← lintegral_add_compl (fun theta => K theta (retentionFailureSet (X := X) (Y := Y) n m)) hA] apply add_le_add · calc (∫⁻ theta in A, K theta (retentionFailureSet (X := X) (Y := Y) n m) ∂pi) ≤ ∫⁻ _theta in A, 1 ∂pi := by apply lintegral_mono intro theta change K theta (retentionFailureSet (X := X) (Y := Y) n m) ≤ 1 rw [hraw theta] exact prob_le_one _ = pi A := by simp · rw [hAc] apply lintegral_mono intro theta exact conditional_retentionFailure_le_poissonLowerTails K P Q S u v hraw n m theta

theorem map_orderedPrefix_finitePoissonSampleLaw (P : Measure X) [IsProbabilityMeasure P] (lam : ℝ≥0) (fallback : Fin n → X) : Measure.map (orderedPrefix fallback) (finitePoissonSampleLaw P lam) = poissonMeasure lam (Set.Ici n) • Measure.pi (fun _ : Fin n => P) + poissonMeasure lam (Set.Iio n) • Measure.dirac fallback := by let μ := finitePoissonSampleLaw P lam let good : Set (FiniteSample X) := FiniteSample.count ⁻¹' Set.Ici n let bad : Set (FiniteSample X) := FiniteSample.count ⁻¹' Set.Iio n have hgood_meas : MeasurableSet good := (by measurability : MeasurableSet (Set.Ici n)).preimage measurable_finiteSample_count have hbad_meas : MeasurableSet bad := (by measurability : MeasurableSet (Set.Iio n)).preimage measurable_finiteSample_count have hgood : Measure.map (orderedPrefix fallback) (μ.restrict good) = poissonMeasure lam (Set.Ici n) • Measure.pi (fun _ : Fin n => P) := map_orderedPrefix_restrict_count_ge P lam fallback have hbad : Measure.map (orderedPrefix fallback) (μ.restrict bad) = poissonMeasure lam (Set.Iio n) • Measure.dirac fallback := by have heq : orderedPrefix fallback =ᵐ[μ.restrict bad] fun _ => fallback := by apply ae_restrict_of_forall_mem hbad_meas intro s hs have hlt : s.count < n := hs simp [orderedPrefix, not_le.mpr hlt] rw [Measure.map_congr heq, Measure.map_const] congr 1 rw [Measure.restrict_apply_univ] change μ (FiniteSample.count ⁻¹' Set.Iio n) = _ rw [show μ = finitePoissonSampleLaw P lam by rfl, ← finitePoissonSampleLaw_map_count P lam, Measure.map_apply measurable_finiteSample_count (by measurability)] have hcompl : bad = goodᶜ := by ext s simp [good, bad] change Measure.map (orderedPrefix fallback) μ = _ rw [← (Measure.restrict_add_restrict_compl hgood_meas : μ.restrict good + μ.restrict goodᶜ = μ), ← hcompl, Measure.map_add _ _ (measurable_orderedPrefix fallback), hgood, hbad]

theorem minimaxDecisionRisk_lower_of_rawBayesTransfer {Z : Type uZ} [MeasurableSpace Z] (Kfixed : Kernel Theta Z) (loss : Theta → A → ℝ≥0∞) (rawLower penalty : ℝ≥0∞) (htransfer : ∀ rule : {f : Z → A // Measurable f}, rawLower ≤ worstCaseDecisionRisk Kfixed loss rule.1 + penalty) : rawLower - penalty ≤ minimaxDecisionRisk Kfixed loss := by /- For each measurable rule, residuation for truncated subtraction turns `htransfer` into `rawLower - penalty ≤ worst-case risk`. Take the infimum over rules. -/ unfold minimaxDecisionRisk apply le_iInf intro rule apply tsub_le_iff_left.mpr simpa [add_comm] using htransfer rule