Formalization: Second-order Minimax Risk in Multi-arm Binary Randomization

lemma Lc_pos (c : Contrast ℝ K) : 0 < Lc c := by have hnonneg : 0 ≤ Lc c := sum_nonneg fun _ _ => abs_nonneg _ have hne : Lc c ≠ 0 := by intro hsum apply c.nonzero funext a apply abs_eq_zero.mp exact congrFun ((Fintype.sum_eq_zero_iff_of_nonneg (fun a => abs_nonneg (c a))).mp hsum) a exact lt_of_le_of_ne hnonneg (Ne.symm hne)

lemma bayesianInformation_ae_section_nonnegative {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) {ell u : ℝ} {p : ℝ → Ω → ℝ} (hn : ∀ θ, θ ∈ Ioo ell u → ∀ᵐ x ∂μ, 0 ≤ p θ x) (hac : ∀ᵐ x ∂μ, ∀ a ∈ Ioo ell u, ∀ b ∈ Ioo ell u, AbsolutelyContinuousOnInterval (fun θ => p θ x) a b) : ∀ᵐ x ∂μ, ∀ θ, θ ∈ Ioo ell u → 0 ≤ p θ x := by have hrat : ∀ᵐ x ∂μ, ∀ q : ℚ, ((q : ℝ) ∈ Ioo ell u → 0 ≤ p q x) := by rw [ae_all_iff] intro q by_cases hq : (q : ℝ) ∈ Ioo ell u · exact (hn q hq).mono (fun _ hx _ => hx) · exact Filter.Eventually.of_forall (fun _ h => (hq h).elim) filter_upwards [hac, hrat] with x hxac hxrat intro θ hθ rcases hθ with ⟨hellθ, hθu⟩ obtain ⟨q, _hqmono, hqθ, hqlim⟩ := Rat.denseRange_cast.exists_seq_strictMono_tendsto Rat.cast_mono θ let a := (ell + θ) / 2 let b := (θ + u) / 2 have ha : a ∈ Ioo ell u := by dsimp [a]; constructor <;> linarith have hb : b ∈ Ioo ell u := by dsimp [b]; constructor <;> linarith have hab : a < b := by dsimp [a, b]; linarith have hθab : θ ∈ Ioo a b := by dsimp [a, b]; constructor <;> linarith have hcont : ContinuousAt (fun s => p s x) θ := (hxac a ha b hb).continuousOn.continuousAt (by simpa [hab.le] using Icc_mem_nhds hθab.1 hθab.2) apply isClosed_Ici.mem_of_tendsto (hcont.tendsto.comp hqlim) filter_upwards [(tendsto_order.1 hqlim).1 a hθab.1] with n hn exact hxrat (q n) ⟨ha.1.trans hn, (hqθ n).trans hθu⟩

lemma bayesianInformationInequality {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [SigmaFinite μ] (ell u : ℝ) (w dw : ℝ → ℝ) (p dp g dg : ℝ → Ω → ℝ) (T : Ω → ℝ) (h : BayesianInformationRegularity μ ell u w dw p dp g dg T) : bayesJointIntegral μ ell u w p (fun θ x => (T x - g θ x) ^ 2) ≥ bayesJointIntegral μ ell u w p dg ^ 2 / (priorInformation ell u w dw + ∫ θ in ell..u, fisherInformation μ p dp θ * w θ) := by let PM := Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure have hsupport : support w ⊆ Icc ell u := by intro θ hθ exact ⟨le_of_lt (h.prior_compact_support.2 (subset_tsupport w hθ)).1, le_of_lt (h.prior_compact_support.2 (subset_tsupport w hθ)).2⟩ have hwderiv : ∀ θ, HasDerivAt w (dw θ) θ := by intro θ rw [h.prior_derivative θ] exact (h.prior_C1.differentiable (by norm_num)).differentiableAt.hasDerivAt have hwnorm : ∫ θ, w θ ∂PM ell u = 1 := by rw [← h.prior_probability, intervalIntegral.integral_of_le h.interval_nonempty.le] unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure rw [restrict_Ioc_eq_restrict_Icc] have hboundary : ∀ᵐ x ∂μ, w u * p u x * (T x - g u x) = 0 ∧ w ell * p ell x * (T x - g ell x) = 0 := by filter_upwards [h.boundary_vanishes_ae] with x hx exact ⟨hx.2, hx.1⟩ have hsensitivityInt : Integrable (sensitivityField w p dg) ((PM ell u).prod μ) := by change Integrable (sensitivityField w p dg) ((volume.restrict (Icc ell u)).prod μ) convert h.derivative_joint_integrable using 1 ext z simp [sensitivityField, jointDensity] ring have herrorSqInt : Integrable (errorSqField w p g T) ((PM ell u).prod μ) := by change Integrable (errorSqField w p g T) ((volume.restrict (Icc ell u)).prod μ) convert h.risk_joint_integrable using 1 ext z simp [errorSqField, jointDensity] ring letI : IsFiniteMeasure (PM ell u) := by unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure infer_instance have hrisk : bayesJointIntegral μ ell u w p (fun θ x => (T x - g θ x) ^ 2) = ∫ z, errorSqField w p g T z ∂((PM ell u).prod μ) := by calc _ = ∫ θ, ∫ x, (T x - g θ x) ^ 2 * p θ x * w θ ∂μ ∂PM ell u := by rw [bayesJointIntegral, intervalIntegral.integral_of_le h.interval_nonempty.le] unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure rw [restrict_Ioc_eq_restrict_Icc] _ = _ := by rw [MeasureTheory.integral_prod _ herrorSqInt] apply MeasureTheory.integral_congr_ae filter_upwards with θ apply MeasureTheory.integral_congr_ae filter_upwards with x simp [errorSqField, jointDensity] ring have hsensitivity : bayesJointIntegral μ ell u w p dg = ∫ z, sensitivityField w p dg z ∂((PM ell u).prod μ) := by calc _ = ∫ θ, ∫ x, dg θ x * p θ x * w θ ∂μ ∂PM ell u := by rw [bayesJointIntegral, intervalIntegral.integral_of_le h.interval_nonempty.le] unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure rw [restrict_Ioc_eq_restrict_Icc] _ = _ := by rw [MeasureTheory.integral_prod _ hsensitivityInt] apply MeasureTheory.integral_congr_ae filter_upwards with θ apply MeasureTheory.integral_congr_ae filter_upwards with x simp [sensitivityField, jointDensity] ring have hprior : priorInformation ell u w dw = priorInformation ell u w dw := by rw [priorInformation, priorInformation, intervalIntegral.integral_of_le h.interval_nonempty.le] rw [Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure, ← restrict_Ioc_eq_restrict_Icc] apply MeasureTheory.integral_congr_ae filter_upwards with θ simp [priorScore] split_ifs with hθ · field_simp · ring have hfisher : (∫ θ in ell..u, fisherInformation μ p dp θ * w θ) = ∫ θ, w θ * fisherInformation μ p dp θ ∂PM ell u := by rw [intervalIntegral.integral_of_le h.interval_nonempty.le] unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure rw [restrict_Ioc_eq_restrict_Icc] apply MeasureTheory.integral_congr_ae filter_upwards with θ have hFI : fisherInformation μ p dp θ = fisherInformation μ p dp θ := by rw [fisherInformation, fisherInformation] apply MeasureTheory.integral_congr_ae filter_upwards with x simp [likelihoodScore] split_ifs with hx · field_simp · ring rw [hFI, mul_comm] have hinfoPos : 0 < priorInformation ell u w dw + ∫ θ, w θ * fisherInformation μ p dp θ ∂PM ell u := by rw [← hprior, ← hfisher] exact h.total_information_positive have hvt : (∫ z, sensitivityField w p dg z ∂((PM ell u).prod μ)) ^ 2 / (priorInformation ell u w dw + ∫ θ, w θ * fisherInformation μ p dp θ ∂PM ell u) ≤ ∫ z, errorSqField w p g T z ∂((PM ell u).prod μ) := by letI : IsFiniteMeasure (PM ell u) := by unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure infer_instance have hmemIcc : ∀ᵐ θ ∂PM ell u, θ ∈ Icc ell u := by unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure exact ae_restrict_mem measurableSet_Icc have hmemIoo : ∀ᵐ θ ∂PM ell u, θ ∈ Ioo ell u := by filter_upwards [hmemIcc, (by unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure exact ae_restrict_of_ae (volume.ae_ne ell)), (by unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure exact ae_restrict_of_ae (volume.ae_ne u))] with θ hθ hθell hθu exact ⟨lt_of_le_of_ne hθ.1 (Ne.symm hθell), lt_of_le_of_ne hθ.2 hθu⟩ have hpSections : ∀ᵐ x ∂μ, ∀ θ, θ ∈ Ioo ell u → 0 ≤ p θ x := bayesianInformation_ae_section_nonnegative μ h.density_nonnegative h.likelihood_ac_ae have hpNonneg : ∀ᵐ z ∂((PM ell u).prod μ), 0 ≤ p z.1 z.2 := by have hx : ∀ᵐ z ∂((PM ell u).prod μ), ∀ θ, θ ∈ Ioo ell u → 0 ≤ p θ z.2 := Measure.quasiMeasurePreserving_snd.tendsto_ae.eventually hpSections have hθ : ∀ᵐ z ∂((PM ell u).prod μ), z.1 ∈ Ioo ell u := Measure.quasiMeasurePreserving_fst.tendsto_ae.eventually hmemIoo filter_upwards [hx, hθ] with z hxz hθz exact hxz z.1 hθz have hwzero : ∀ θ, w θ = 0 → dw θ = 0 := by intro θ hzero exact derivative_eq_zero_of_nonnegative_of_eq_zero h.prior_nonnegative (hwderiv θ) hzero have hpzero : ∀ᵐ z ∂((PM ell u).prod μ), p z.1 z.2 = 0 → dp z.1 z.2 = 0 := by have hx : ∀ᵐ z ∂((PM ell u).prod μ), ∀ θ, θ ∈ Ioo ell u → 0 ≤ p θ z.2 := Measure.quasiMeasurePreserving_snd.tendsto_ae.eventually hpSections have hθ : ∀ᵐ z ∂((PM ell u).prod μ), z.1 ∈ Ioo ell u := Measure.quasiMeasurePreserving_fst.tendsto_ae.eventually hmemIoo have hderiv : ∀ᵐ z ∂((PM ell u).prod μ), HasDerivAt (fun t => p t z.2) (dp z.1 z.2) z.1 := by simpa [PM, Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure, restrict_Ioo_eq_restrict_Icc] using h.likelihood_hasDerivAt_ae filter_upwards [hderiv, hx, hθ] with z hder hxz hθz intro hz have hmin : IsLocalMin (fun t => p t z.2) z.1 := by filter_upwards [Ioo_mem_nhds hθz.1 hθz.2] with t ht rw [hz] exact hxz t ht exact hmin.hasDerivAt_eq_zero hder have hdpSwap : ∀ᵐ z ∂(μ.prod (PM ell u)), HasDerivAt (fun t => p t z.1) (dp z.2 z.1) z.2 := by have hderiv : ∀ᵐ z ∂((PM ell u).prod μ), HasDerivAt (fun t => p t z.2) (dp z.1 z.2) z.1 := by simpa [PM, Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure, restrict_Ioo_eq_restrict_Icc] using h.likelihood_hasDerivAt_ae have hz := Measure.measurePreserving_swap.quasiMeasurePreserving.tendsto_ae.eventually hderiv simpa [swap] using hz have hdgSwap : ∀ᵐ z ∂(μ.prod (PM ell u)), HasDerivAt (fun t => g t z.1) (dg z.2 z.1) z.2 := by have hderiv : ∀ᵐ z ∂((PM ell u).prod μ), HasDerivAt (fun t => g t z.2) (dg z.1 z.2) z.1 := by simpa [PM, Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure, restrict_Ioo_eq_restrict_Icc] using h.target_hasDerivAt_ae have hz := Measure.measurePreserving_swap.quasiMeasurePreserving.tendsto_ae.eventually hderiv simpa [swap] using hz have hdpSections : ∀ᵐ x ∂μ, ∀ᵐ θ ∂PM ell u, HasDerivAt (fun t => p t x) (dp θ x) θ := by simpa using Measure.ae_ae_of_ae_prod hdpSwap have hdgSections : ∀ᵐ x ∂μ, ∀ᵐ θ ∂PM ell u, HasDerivAt (fun t => g t x) (dg θ x) θ := by simpa using Measure.ae_ae_of_ae_prod hdgSwap have hbalanceZero : ∫ z, derivativeBalanceField w dw p dp g dg T z ∂((PM ell u).prod μ) = 0 := by have hbalanceInt : Integrable (derivativeBalanceField w dw p dp g dg T) ((PM ell u).prod μ) := by simpa [PM, Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure] using h.derivative_balance_joint_integrable rw [integral_prod_symm _ hbalanceInt] apply integral_eq_zero_of_ae filter_upwards [h.product_ac_ae, hboundary, hdpSections, hdgSections, hbalanceInt.prod_left_ae] with x hacx hboundaryx hdpx hdgx hintx let q : ℝ → ℝ := fun θ => w θ * p θ x * (T x - g θ x) have hqderiv : ∀ᵐ θ ∂PM ell u, HasDerivAt q (derivativeBalanceField w dw p dp g dg T (θ, x)) θ := by filter_upwards [hdpx, hdgx] with θ hdpθ hdgθ have hm := ((hwderiv θ).mul hdpθ).mul (hdgθ.const_sub (T x)) simp only [Pi.mul_apply] at hm have hfun : q = (w * (fun t => p t x)) * (fun t => T x - g t x) := by funext t rfl have hcoef : derivativeBalanceField w dw p dp g dg T (θ, x) = (dw θ * p θ x + w θ * dp θ x) * (T x - g θ x) + w θ * p θ x * -dg θ x := by simp [derivativeBalanceField, jointDensity] ring rw [hfun, hcoef] exact hm calc (∫ θ, derivativeBalanceField w dw p dp g dg T (θ, x) ∂PM ell u) = ∫ θ, deriv q θ ∂PM ell u := by apply integral_congr_ae filter_upwards [hqderiv] with θ hθ exact hθ.deriv.symm _ = ∫ θ in ell..u, deriv q θ := by unfold PM Causalean.Stat.Limit.ObservationDependentVanTrees.parameterMeasure rw [intervalIntegral.integral_of_le h.interval_nonempty.le, restrict_Ioc_eq_restrict_Icc] _ = q u - q ell := hacx.integral_deriv_eq_sub _ = 0 := by simp [q, hboundaryx.1, hboundaryx.2] have herrorSensitivity : -- … truncated; follow the source link for the rest …

lemma positiveCoefficientSum (c : Contrast ℝ K) : ∑ a with 0 < c a, c a = signGroupScale c := by classical let P : ℝ := ∑ a with 0 < c a, c a let N : ℝ := ∑ a with c a < 0, c a have hsum : P + N = 0 := by rw [← c.sum_zero] dsimp [P, N] simp only [Finset.sum_filter, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro a _ by_cases hp : 0 < c a · simp [hp, not_lt.mpr hp.le] · by_cases hn : c a < 0 · simp [hp, hn] · have hz : c a = 0 := le_antisymm (le_of_not_gt hp) (le_of_not_gt hn) simp [hp, hn, hz] have habs : Lc c = P - N := by unfold Lc dsimp [P, N] simp only [Finset.sum_filter, ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro a _ by_cases hp : 0 < c a · simp [hp, not_lt.mpr hp.le, abs_of_pos hp] · by_cases hn : c a < 0 · simp [hp, hn, abs_of_neg hn] · have hz : c a = 0 := le_antisymm (le_of_not_gt hp) (le_of_not_gt hn) simp [hp, hn, hz] unfold signGroupScale dsimp [P, N] at hsum habs ⊢ linarith

lemma negativeCoefficientSum (c : Contrast ℝ K) : ∑ a with c a < 0, c a = -signGroupScale c := by have hp := positiveCoefficientSum c have hs : (∑ a with 0 < c a, c a) + (∑ a with c a < 0, c a) = 0 := by classical calc _ = ∑ a, c a := by simp only [Finset.sum_filter, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro a _ by_cases hpa : 0 < c a · simp [hpa, not_lt.mpr hpa.le] · by_cases hna : c a < 0 · simp [hpa, hna] · have hz : c a = 0 := le_antisymm (le_of_not_gt hpa) (le_of_not_gt hna) simp [hpa, hna, hz] _ = 0 := c.sum_zero linarith

lemma embeddedSignSchedule_observation (c : Contrast ℝ K) (z : Schedule 2 n) (w : Assign K n × (Unit n → Bool)) : inactiveZeroObservation c w.1 (obsOutcome z (signGroupAssignment c w)) = obsOutcome (embeddedSignSchedule c z) w.1 := by funext i unfold inactiveZeroObservation obsOutcome potentialOutcome signGroupAssignment embeddedSignSchedule by_cases hp : 0 < c (w.1 i) · simp [hp, ne_of_gt hp] by_cases hn : c (w.1 i) < 0 · simp [hp, hn, ne_of_lt hn] have hz : c (w.1 i) = 0 := le_antisymm (le_of_not_gt hp) (le_of_not_gt hn) simp [hp, hn, hz]

lemma embeddedSignSchedule_target (c : Contrast ℝ K) (z : Schedule 2 n) : tauC c (embeddedSignSchedule c z) = signGroupScale c * tauC twoArmContrast z := by classical have hi (i : Unit n) : (∑ a, c a * if embeddedSignSchedule c z i a then 1 else 0) = signGroupScale c * (∑ a, twoArmContrast a * if z i a then 1 else 0) := by have hp := positiveCoefficientSum c have hn := negativeCoefficientSum c cases z0 : z i 0 <;> cases z1 : z i 1 <;> simp [embeddedSignSchedule, twoArmContrast, ratContrastToReal, twoArmContrastQ, Fin.sum_univ_succ, z0, z1, Finset.sum_filter] at hp hn ⊢ · simpa [and_iff_right_of_imp (fun h : c _ < 0 => h.le)] using hn · exact hp · calc (∑ x, if 0 = c x then 0 else c x) = ∑ x, c x := by apply Finset.sum_congr rfl intro a _ by_cases hz : c a = 0 <;> simp [hz] _ = 0 := c.sum_zero unfold tauC simp_rw [hi] simp_rw [← mul_assoc] rw [← Finset.mul_sum] ring

lemma signLatentDesign_E_fst (D : FiniteDesign (Assign K n)) (f : Assign K n → ℝ) : (signLatentDesign D).E (fun w => f w.1) = D.E f := by classical rw [signLatentDesign, FiniteDesign.E_compound] unfold FiniteDesign.E apply Finset.sum_congr rfl intro A _ calc (∑ s : Unit n → Bool, D.p A * (∏ i, fairBoolDesign.p (s i)) * f A) = D.p A * f A * ∑ s : Unit n → Bool, ∏ i, fairBoolDesign.p (s i) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro s _ ring _ = D.p A * f A := by rw [show (∑ s : Unit n → Bool, ∏ i, fairBoolDesign.p (s i)) = 1 from (prodDesign (fun _ : Unit n => fairBoolDesign)).p_sum, mul_one]

lemma scaledLatentEstimator_mem_Icc (c : Contrast ℝ K) (p : Procedure K n c) (w : Assign K n × (Unit n → Bool)) (y : ObservedOutcome n) : scaledLatentEstimator c p w y ∈ Icc (-1 : ℝ) 1 := by have ha := signGroupScale_pos c have hv := (p.2 w.1 (inactiveZeroObservation c w.1 y)).property unfold scaledLatentEstimator constructor · rw [inv_mul_eq_div] apply (le_div_iff₀ ha).2 simpa only [neg_one_mul, signGroupScale, neg_div] using hv.1 · rw [inv_mul_eq_div] apply (div_le_iff₀ ha).2 simpa only [one_mul, signGroupScale] using hv.2

lemma inducedTwoArmProcedure_statewiseRisk (c : Contrast ℝ K) (p : Procedure K n c) (z : Schedule 2 n) : labeledRisk twoArmContrast (inducedTwoArmProcedure c p) z ≤ (signGroupScale c)⁻¹ ^ 2 * labeledRisk c p (embeddedSignSchedule c z) := by let D := signLatentDesign p.1 let φ := signGroupAssignment (n := n) c let v : Assign 2 n → ObservedOutcome n := fun b => obsOutcome z b have hRB := E_map_conditionalMeanAlongMap_sq_le D φ 0 (scaledLatentEstimator c p) v (tauC twoArmContrast z) unfold labeledRisk FiniteDesign.mse inducedTwoArmProcedure change (D.map φ).E (fun b => (conditionalMeanAlongMap D φ 0 (scaledLatentEstimator c p) b (v b) - tauC twoArmContrast z) ^ 2) ≤ _ refine hRB.trans ?_ rw [show D.E (fun w => (scaledLatentEstimator c p w (v (φ w)) - tauC twoArmContrast z) ^ 2) = D.E (fun w => (signGroupScale c)⁻¹ ^ 2 * (((p.2 w.1 (obsOutcome (embeddedSignSchedule c z) w.1) : ℝ) - tauC c (embeddedSignSchedule c z)) ^ 2)) by apply D.E_congr intro w unfold scaledLatentEstimator rw [show v (φ w) = obsOutcome z (signGroupAssignment c w) by rfl, embeddedSignSchedule_observation] rw [embeddedSignSchedule_target] field_simp [(signGroupScale_pos c).ne']] rw [D.E_const_mul] change (signGroupScale c)⁻¹ ^ 2 * D.E (fun w => ((p.2 w.1 (obsOutcome (embeddedSignSchedule c z) w.1) : ℝ) - tauC c (embeddedSignSchedule c z)) ^ 2) ≤ _ rw [show D.E (fun w => ((p.2 w.1 (obsOutcome (embeddedSignSchedule c z) w.1) : ℝ) - tauC c (embeddedSignSchedule c z)) ^ 2) = p.1.E (fun A => ((p.2 A (obsOutcome (embeddedSignSchedule c z) A) : ℝ) - tauC c (embeddedSignSchedule c z)) ^ 2) by simpa [D] using signLatentDesign_E_fst p.1 (fun A => ((p.2 A (obsOutcome (embeddedSignSchedule c z) A) : ℝ) - tauC c (embeddedSignSchedule c z)) ^ 2)]

lemma inducedTwoArmProcedure_worstCaseRisk (c : Contrast ℝ K) (p : Procedure K n c) : worstCaseRisk (fun (q : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => labeledRisk twoArmContrast q z) (inducedTwoArmProcedure c p) ≤ (signGroupScale c)⁻¹ ^ 2 * worstCaseRisk (fun (q : Procedure K n c) (z : Schedule K n) => labeledRisk c q z) p := by apply worstCaseRisk_le intro z calc labeledRisk twoArmContrast (inducedTwoArmProcedure c p) z ≤ (signGroupScale c)⁻¹ ^ 2 * labeledRisk c p (embeddedSignSchedule c z) := inducedTwoArmProcedure_statewiseRisk c p z _ ≤ (signGroupScale c)⁻¹ ^ 2 * worstCaseRisk (fun (q : Procedure K n c) (z : Schedule K n) => labeledRisk c q z) p := by gcongr exact le_worstCaseRisk (Finite.bddAbove_range _) _

lemma embeddedTwoArmLowerBound (K n : ℕ) (c : Contrast ℝ K) : C0 c * rho2 n ≤ rhoN K n c := by let _ : Nonempty (Procedure K n c) := ⟨contrastWeightedProcedure K n c⟩ unfold rho2 rhoN rw [← signGroupScale_sq c] apply Causalean.Stat.le_minimaxValue intro p have hmin : minimaxValue (fun (q : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => labeledRisk twoArmContrast q z) ≤ worstCaseRisk (fun (q : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => labeledRisk twoArmContrast q z) (inducedTwoArmProcedure c p) := minimaxValue_le_worstCaseRisk_of_nonneg (fun q z => q.1.mse_nonneg _ _) _ have h := hmin.trans (inducedTwoArmProcedure_worstCaseRisk c p) have ha : signGroupScale c ≠ 0 := (signGroupScale_pos c).ne' calc signGroupScale c ^ 2 * minimaxValue (fun (q : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => labeledRisk twoArmContrast q z) ≤ signGroupScale c ^ 2 * ((signGroupScale c)⁻¹ ^ 2 * worstCaseRisk (fun (q : Procedure K n c) (z : Schedule K n) => labeledRisk c q z) p) := mul_le_mul_of_nonneg_left h (sq_nonneg _) _ = worstCaseRisk (fun (q : Procedure K n c) (z : Schedule K n) => labeledRisk c q z) p := by field_simp [ha]

lemma exists_positive_contrast_arm (c : Contrast ℝ K) : ∃ a, 0 < c a := by by_contra h push_neg at h have hp := positiveCoefficientSum c have hempty : Finset.univ.filter (fun a => 0 < c a) = ∅ := Finset.filter_eq_empty_iff.mpr (fun a _ => not_lt.mpr (h a)) simp only [hempty, Finset.sum_empty] at hp exact (signGroupScale_pos c).ne' hp.symm

lemma exists_negative_contrast_arm (c : Contrast ℝ K) : ∃ a, c a < 0 := by by_contra h push_neg at h have hn := negativeCoefficientSum c have hempty : Finset.univ.filter (fun a => c a < 0) = ∅ := Finset.filter_eq_empty_iff.mpr (fun a _ => not_lt.mpr (h a)) simp only [hempty, Finset.sum_empty] at hn exact (signGroupScale_pos c).ne' (neg_eq_zero.mp hn.symm)

lemma support_eq_positive_negative_of_card_two (c : Contrast ℝ K) (hcard : (Sc c).card = 2) : Sc c = {positiveContrastArm c, negativeContrastArm c} := by symm apply Finset.eq_of_subset_of_card_le · intro a ha simp only [Finset.mem_insert, mem_singleton] at ha rcases ha with rfl | rfl · exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, (positiveContrastArm_pos c).ne'⟩ · exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, (negativeContrastArm_neg c).ne⟩ · rw [hcard] have hne : positiveContrastArm c ≠ negativeContrastArm c := by intro h have hp := positiveContrastArm_pos c rw [h] at hp linarith [negativeContrastArm_neg c] simp [hne]

lemma coefficient_eq_zero_of_card_two (c : Contrast ℝ K) (hcard : (Sc c).card = 2) {a : Arm K} (haP : a ≠ positiveContrastArm c) (haN : a ≠ negativeContrastArm c) : c a = 0 := by by_contra ha have hm : a ∈ Sc c := Finset.mem_filter.mpr ⟨Finset.mem_univ _, ha⟩ rw [support_eq_positive_negative_of_card_two c hcard] at hm simpa [haP, haN] using hm

lemma positiveContrastArm_coeff (c : Contrast ℝ K) (hcard : (Sc c).card = 2) : c (positiveContrastArm c) = signGroupScale c := by have hp := positiveCoefficientSum c classical rw [show (∑ a with 0 < c a, c a) = c (positiveContrastArm c) by rw [Finset.sum_eq_single (positiveContrastArm c)] · intro b hb hne have hb0 := coefficient_eq_zero_of_card_two c hcard hne (fun h => by rw [h] at hb linarith [negativeContrastArm_neg c, (Finset.mem_filter.mp hb).2]) simp [hb0] · simp [positiveContrastArm_pos c] ] at hp exact hp

lemma negativeContrastArm_coeff (c : Contrast ℝ K) (hcard : (Sc c).card = 2) : c (negativeContrastArm c) = -signGroupScale c := by have hn := negativeCoefficientSum c classical rw [show (∑ a with c a < 0, c a) = c (negativeContrastArm c) by rw [Finset.sum_eq_single (negativeContrastArm c)] · intro b hb hne have hb0 := coefficient_eq_zero_of_card_two c hcard (fun h => by rw [h] at hb linarith [positiveContrastArm_pos c, (Finset.mem_filter.mp hb).2]) hne simp [hb0] · simp [negativeContrastArm_neg c] ] at hn exact hn

lemma positiveContrastArm_ne_negativeContrastArm (c : Contrast ℝ K) : positiveContrastArm c ≠ negativeContrastArm c := by intro h have hp := positiveContrastArm_pos c rw [h] at hp linarith [negativeContrastArm_neg c]

lemma activeToTwo_twoToActive (c : Contrast ℝ K) (B : Assign 2 n) : activeToTwoAssignment c (twoToActiveAssignment c B) = B := by funext i generalize hB : B i = b fin_cases b · simp [activeToTwoAssignment, twoToActiveAssignment, hB] · simp [activeToTwoAssignment, twoToActiveAssignment, hB, (positiveContrastArm_ne_negativeContrastArm c).symm]

lemma activeSchedule_target (c : Contrast ℝ K) (hcard : (Sc c).card = 2) (z : Schedule K n) : tauC c z = signGroupScale c * tauC twoArmContrast (activeSchedule c z) := by classical have hi (i : Unit n) : (∑ a, c a * if z i a then 1 else 0) = signGroupScale c * (∑ b, twoArmContrast b * if activeSchedule c z i b then 1 else 0) := by rw [show (∑ a, c a * if z i a then 1 else 0) = c (positiveContrastArm c) * (if z i (positiveContrastArm c) then 1 else 0) + c (negativeContrastArm c) * (if z i (negativeContrastArm c) then 1 else 0) by calc _ = ∑ a ∈ {positiveContrastArm c, negativeContrastArm c}, c a * if z i a then 1 else 0 := by symm apply Finset.sum_subset (by simp) intro a _ ha have haP : a ≠ positiveContrastArm c := fun h => ha (by simp [h]) have haN : a ≠ negativeContrastArm c := fun h => ha (by simp [h]) simp [coefficient_eq_zero_of_card_two c hcard haP haN] _ = _ := by have hne : positiveContrastArm c ≠ negativeContrastArm c := by intro h have hp := positiveContrastArm_pos c rw [h] at hp linarith [negativeContrastArm_neg c] simp [hne]] rw [positiveContrastArm_coeff c hcard, negativeContrastArm_coeff c hcard] simp [activeSchedule, twoArmContrast, ratContrastToReal, twoArmContrastQ, Fin.sum_univ_succ] by_cases hP : z i (positiveContrastArm c) <;> by_cases hN : z i (negativeContrastArm c) <;> simp [hP, hN] <;> ring unfold tauC simp_rw [hi, ← mul_assoc] rw [← Finset.mul_sum] ring

lemma liftTwoArmProcedure_statewiseRisk (c : Contrast ℝ K) (hcard : (Sc c).card = 2) (p : Procedure 2 n twoArmContrast) (z : Schedule K n) : labeledRisk c (liftTwoArmProcedure c p) z = signGroupScale c ^ 2 * labeledRisk twoArmContrast p (activeSchedule c z) := by unfold labeledRisk FiniteDesign.mse liftTwoArmProcedure rw [p.1.E_map] rw [← p.1.E_const_mul] apply p.1.E_congr intro B change (signGroupScale c * (p.2 (activeToTwoAssignment c (twoToActiveAssignment c B)) (obsOutcome z (twoToActiveAssignment c B)) : ℝ) - tauC c z) ^ 2 = signGroupScale c ^ 2 * ((p.2 B (obsOutcome (activeSchedule c z) B) : ℝ) - tauC twoArmContrast (activeSchedule c z)) ^ 2 rw [activeToTwo_twoToActive, activeSchedule_observation, activeSchedule_target c hcard] ring

lemma supportTwoUpperBound (K n : ℕ) (c : Contrast ℝ K) (hcard : (Sc c).card = 2) : rhoN K n c ≤ C0 c * rho2 n := by let _ : Nonempty (Procedure 2 n twoArmContrast) := ⟨contrastWeightedProcedure 2 n twoArmContrast⟩ unfold rhoN rho2 rw [← signGroupScale_sq c] let A : ℝ := signGroupScale c ^ 2 have hA : 0 < A := by dsimp [A]; exact sq_pos_of_pos (signGroupScale_pos c) have hscale : A * Causalean.Stat.minimaxValue (fun (p : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => labeledRisk twoArmContrast p z) = Causalean.Stat.minimaxValue (fun (p : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => A * labeledRisk twoArmContrast p z) := by unfold Causalean.Stat.minimaxValue Causalean.Stat.worstCaseRisk have hbdd : BddBelow (range (fun p : Procedure 2 n twoArmContrast => ⨆ z : Schedule 2 n, labeledRisk twoArmContrast p z)) := bddBelow_range_worstCaseRisk (fun (p : Procedure 2 n twoArmContrast) z => p.1.mse_nonneg _ _) calc A * (⨅ p : Procedure 2 n twoArmContrast, ⨆ z : Schedule 2 n, labeledRisk twoArmContrast p z) = ⨅ p : Procedure 2 n twoArmContrast, A * (⨆ z : Schedule 2 n, labeledRisk twoArmContrast p z) := (OrderIso.mulLeft₀ A hA).map_ciInf hbdd _ = ⨅ p : Procedure 2 n twoArmContrast, ⨆ z : Schedule 2 n, A * labeledRisk twoArmContrast p z := by congr with p exact (OrderIso.mulLeft₀ A hA).map_ciSup (Finite.bddAbove_range _) change Causalean.Stat.minimaxValue (fun (p : Procedure K n c) (z : Schedule K n) => labeledRisk c p z) ≤ A * Causalean.Stat.minimaxValue (fun (p : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => labeledRisk twoArmContrast p z) rw [hscale] apply minimaxValue_le_minimaxValue (bddBelow_range_worstCaseRisk (fun p z => p.1.mse_nonneg _ _)) intro p refine ⟨liftTwoArmProcedure c p, ?_⟩ apply worstCaseRisk_le intro z rw [liftTwoArmProcedure_statewiseRisk c hcard] change A * labeledRisk twoArmContrast p (activeSchedule c z) ≤ _ exact le_worstCaseRisk (risk := fun (p : Procedure 2 n twoArmContrast) (z : Schedule 2 n) => A * labeledRisk twoArmContrast p z) (e := p) (Finite.bddAbove_range _) (activeSchedule c z)

lemma finite_orbit_game_has_saddle : HasOrbitSaddle n c := by classical let X : AllocVec K n → Type := fun r => ObsVec r let l : ℝ := -Lc c / 2 let u : ℝ := Lc c / 2 have hK : K ≠ 0 := by intro hK apply c.nonzero funext a exact elim0 (hK ▸ a) letI : Nonempty (Arm K) := Fintype.card_pos_iff.mp (by simpa using Nat.pos_of_ne_zero hK) letI : Nonempty (CountVec K n) := ⟨scheduleCounts (fun _ _ => false)⟩ let a₀ : Arm K := Classical.choice inferInstance let r₀ : AllocVec K n := ⟨fun a => if a = a₀ then ⟨n, Nat.lt_succ_self n⟩ else 0, by rw [Finset.sum_eq_single a₀] · simp · intro b _ hba simp [hba] · simp⟩ letI : Nonempty (AllocVec K n) := ⟨r₀⟩ have hlu : l ≤ u := by dsimp [l, u] have hLc : 0 ≤ Lc c := sum_nonneg fun _ _ => abs_nonneg _ linarith let P : CountVec K n → ∀ r : AllocVec K n, X r → ℝ := fun m r x => (orbitLik m r x : ℝ) let tau : CountVec K n → ℝ := tauCount c have hP : ∀ m r x, 0 ≤ P m r x := by intro m r x change (0 : ℝ) ≤ ((orbitLik m r x : ℚ) : ℝ) exact_mod_cast orbitLik_nonneg m r x let e : OrbitProcedure K n c ≃ Procedure X l u := { toFun := fun q => ⟨q.1, q.2⟩ invFun := fun q => (q.design, q.decision) left_inv := fun _ => rfl right_inv := fun q => by cases q; rfl } have hvalue : minimaxValue (Causalean.Stat.Minimax.FiniteSquaredLoss.risk P tau : Procedure X l u → CountVec K n → ℝ) = orbitGameValue K n c := by unfold orbitGameValue minimaxValue rw [← e.iInf_comp] rfl obtain ⟨qstar, deltastar, nu, hupper, hlower⟩ := finite_bounded_squared_loss_has_saddle P tau hlu hP refine ⟨(qstar, deltastar), nu, ?_, ?_⟩ · intro m change Causalean.Stat.Minimax.FiniteSquaredLoss.risk P tau ⟨qstar, deltastar⟩ m ≤ orbitGameValue K n c rw [← hvalue] exact hupper m · intro q' have h := hlower (e q') rw [hvalue] at h exact h

lemma upperUnitScore_mean (c : Contrast ℝ K) (t : RespType K) : (qStarDesign c).E (upperUnitScore c t) = ∑ a, c a * (if t a then 1 else 0) := by classical unfold E upperUnitScore qStarDesign calc ∑ a, qStar c a * (if qStar c a = 0 then 0 else c a * ((if t a then 1 else 0) - 1 / 2) / qStar c a) = ∑ a, c a * ((if t a then 1 else 0) - 1 / 2) := by apply Finset.sum_congr rfl intro a _ by_cases hc : c a = 0 · simp [qStar, hc] · have hq : qStar c a ≠ 0 := div_ne_zero (abs_ne_zero.mpr hc) (ne_of_gt (Lc_pos c)) rw [if_neg hq] field_simp [hq] _ = ∑ a, c a * (if t a then 1 else 0) := by calc _ = ∑ a, (c a * (if t a then 1 else 0) - c a / 2) := by apply Finset.sum_congr rfl intro a _ ring _ = (∑ a, c a * (if t a then 1 else 0)) - ∑ a, c a / 2 := by rw [Finset.sum_sub_distrib] _ = _ := by rw [← Finset.sum_div, c.sum_zero]; norm_num

lemma upperUnitScore_secondMoment (c : Contrast ℝ K) (t : RespType K) : (qStarDesign c).E (fun a => upperUnitScore c t a ^ 2) = C0 c := by classical unfold E upperUnitScore qStarDesign rw [C0] have hhalf (a : Arm K) : ((if t a then (1 : ℝ) else 0) - 1 / 2) ^ 2 = 1 / 4 := by by_cases ht : t a <;> simp [ht] <;> norm_num calc ∑ a, qStar c a * (if qStar c a = 0 then 0 else c a * ((if t a then 1 else 0) - 1 / 2) / qStar c a) ^ 2 = ∑ a, Lc c * |c a| / 4 := by apply Finset.sum_congr rfl intro a _ by_cases hc : c a = 0 · simp [qStar, hc] · have hq : qStar c a ≠ 0 := div_ne_zero (abs_ne_zero.mpr hc) (ne_of_gt (Lc_pos c)) rw [if_neg hq, div_pow, mul_pow, hhalf] simp only [qStar] field_simp [abs_ne_zero.mpr hc, ne_of_gt (Lc_pos c)] rw [sq_abs] _ = Lc c ^ 2 / 4 := by rw [← Finset.sum_div, ← Finset.mul_sum] simp only [Lc] ring

lemma contrastWeightedProcedure_upperRisk (K n : ℕ) (c : Contrast ℝ K) (hn : 0 < n) : worstCaseRisk (fun (p : Procedure K n c) (z : Schedule K n) => labeledRisk c p z) (contrastWeightedProcedure K n c) ≤ C0 c / n := by classical apply worstCaseRisk_le intro z let D := prodDesign (fun _ : Unit n => qStarDesign c) let raw : Assign K n → ℝ := fun A => (n : ℝ)⁻¹ * ∑ i, upperUnitScore c (z i) (A i) have hunbiased : D.Unbiased raw (tauC c z) := by unfold Unbiased raw D tauC rw [E_const_mul, E_sum] simp_rw [E_prod_apply, upperUnitScore_mean] have hvar : D.Var raw ≤ C0 c / n := by rw [show raw = fun A => ∑ i, (n : ℝ)⁻¹ * upperUnitScore c (z i) (A i) by funext A; simp only [raw]; rw [Finset.mul_sum], Var_prod_linear_comb] calc _ ≤ ∑ _i : Unit n, (n : ℝ)⁻¹ ^ 2 * C0 c := by apply Finset.sum_le_sum intro i _ gcongr rw [Var_eq, upperUnitScore_secondMoment] exact sub_le_self _ (sq_nonneg _) _ = C0 c / n := by simp; field_simp unfold labeledRisk contrastWeightedProcedure change D.mse (fun A => clip c (centeredContrastScore c A (obsOutcome z A))) (tauC c z) ≤ C0 c / n calc _ ≤ D.mse raw (tauC c z) := by unfold mse apply Finset.sum_le_sum intro A _ apply mul_le_mul_of_nonneg_left _ (D.p_nonneg A) change (clip c (centeredContrastScore c A (obsOutcome z A)) - tauC c z) ^ 2 ≤ (raw A - tauC c z) ^ 2 have hraw : centeredContrastScore c A (obsOutcome z A) = raw A := rfl rw [hraw] exact clip_sq_dist_le c _ _ (tauC_mem_naturalInterval c z hn) _ = D.Var raw := D.mse_eq_var_of_unbiased hunbiased _ ≤ _ := hvar