Formalization: Outcome Annotation and Minimax Risk for Discrete Average Treatment Effects

lemma jointMass_mem_unitInterval {d : Nat} (P : DiscreteLaw d) (x : Fin d) (a y : Bool) : jointMass P x a y ∈ Icc (0 : Real) 1 := by constructor · exact ENNReal.toReal_nonneg · exact ENNReal.toReal_le_coe_of_le_coe (P.pmf.coe_le_one (x, a, y))

lemma cellMass_mem_unitInterval {d : Nat} (P : DiscreteLaw d) (x : Fin d) : cellMass P x ∈ Icc (0 : Real) 1 := by have hsum : ∑ z : Obs d, (P.pmf z).toReal = 1 := by simpa using (PMF.integral_eq_sum P.pmf (fun _ : Obs d => (1 : Real))).symm constructor · exact Finset.sum_nonneg fun a _ => Finset.sum_nonneg fun y _ => (jointMass_mem_unitInterval P x a y).1 · calc cellMass P x ≤ ∑ x' : Fin d, cellMass P x' := by exact Finset.single_le_sum (fun i _ => Finset.sum_nonneg fun a _ => Finset.sum_nonneg fun y _ => (jointMass_mem_unitInterval P i a y).1) (Finset.mem_univ x) _ = ∑ z : Obs d, (P.pmf z).toReal := by simp [cellMass, jointMass, Fintype.sum_prod_type] _ = 1 := hsum

lemma outcomeMean_mem_unitInterval {d : Nat} (P : DiscreteLaw d) (a : Bool) (x : Fin d) : outcomeMean P a x ∈ Icc (0 : Real) 1 := by have hj_nonneg : 0 ≤ jointMass P x a true := (jointMass_mem_unitInterval P x a true).1 have harm_nonneg : 0 ≤ armMass P x a := by exact Finset.sum_nonneg fun y _ => (jointMass_mem_unitInterval P x a y).1 have hj_le : jointMass P x a true ≤ armMass P x a := by simp [armMass] exact (jointMass_mem_unitInterval P x a false).1 constructor · exact div_nonneg hj_nonneg harm_nonneg · exact div_le_one_of_le₀ hj_le harm_nonneg

lemma ateFunctional_mem_Icc_neg_one_one {d : Nat} {eps : Real} (P : DiscreteLaw d) (hP : Overlap eps P) : ateFunctional P ∈ Icc (-1 : Real) 1 := by have hsum : ∑ x : Fin d, cellMass P x = 1 := by have htotal : ∑ z : Obs d, (P.pmf z).toReal = 1 := by simpa using (PMF.integral_eq_sum P.pmf (fun _ : Obs d => (1 : Real))).symm calc ∑ x : Fin d, cellMass P x = ∑ z : Obs d, (P.pmf z).toReal := by simp [cellMass, jointMass, Fintype.sum_prod_type] _ = 1 := htotal have habs : |ateFunctional P| ≤ 1 := by rw [ateFunctional] calc |∑ x : Fin d, cellMass P x * (outcomeMean P true x - outcomeMean P false x)| ≤ ∑ x : Fin d, |cellMass P x * (outcomeMean P true x - outcomeMean P false x)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ x : Fin d, cellMass P x := by apply Finset.sum_le_sum intro x _ have hp := cellMass_mem_unitInterval P x have hm1 := outcomeMean_mem_unitInterval P true x have hm0 := outcomeMean_mem_unitInterval P false x rcases hm1 with ⟨hm1lo, hm1hi⟩ rcases hm0 with ⟨hm0lo, hm0hi⟩ rw [abs_mul, abs_of_nonneg hp.1] apply mul_le_of_le_one_right hp.1 rw [abs_le] constructor <;> linarith _ = 1 := hsum exact abs_le.mp habs

lemma observedMarginal_jointMass {d : Nat} (Q : PotentialLaw d) (x : Fin d) (a y : Bool) : jointMass (observedMarginal Q) x a y = ∑ y0 : Bool, ∑ y1 : Bool, fullMass Q (x, a, y, y0, y1) := by classical unfold jointMass observedMarginal fullMass rw [PMF.map_apply, tsum_fintype] cases a <;> cases y <;> simp only [Fintype.sum_prod_type] <;> simp all_goals rw [ENNReal.toReal_add (ENNReal.add_ne_top.mpr ⟨Q.pmf.apply_ne_top _, Q.pmf.apply_ne_top _⟩) (ENNReal.add_ne_top.mpr ⟨Q.pmf.apply_ne_top _, Q.pmf.apply_ne_top _⟩), ENNReal.toReal_add (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _), ENNReal.toReal_add (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)]

-- @node: ateFunctional_observedMarginal_eq_po_contrast lemma ateFunctional_observedMarginal_eq_po_contrast {d : Nat} {eps : Real} (Q : PotentialLaw d) (heps : 0 < eps) (hCons : Consistency Q) (hExch : ConditionalExchangeability Q) (hOv : Overlap eps (observedMarginal Q)) : ateFunctional (observedMarginal Q) = ∑ z : FullObs d, fullMass Q z * ((if z.2.2.2.2 then (1 : Real) else 0) - (if z.2.2.2.1 then (1 : Real) else 0)) := by classical rw [ateFunctional] simp only [Fintype.sum_prod_type] apply Finset.sum_congr rfl intro x _ have hc_tf (y0 : Bool) : fullMass Q (x, true, false, y0, true) = 0 := hCons _ (by simp) have hc_tt (y0 : Bool) : fullMass Q (x, true, true, y0, false) = 0 := hCons _ (by simp) have hc_ff (y1 : Bool) : fullMass Q (x, false, false, true, y1) = 0 := hCons _ (by simp) have hc_ft (y1 : Bool) : fullMass Q (x, false, true, false, y1) = 0 := hCons _ (by simp) have hcellarm : cellMass (observedMarginal Q) x = armMass (observedMarginal Q) x false + armMass (observedMarginal Q) x true := by simp [cellMass, armMass, Fintype.sum_bool] ring by_cases hcx : cellMass (observedMarginal Q) x = 0 · have htotal : (∑ a : Bool, ∑ y0 : Bool, ∑ y1 : Bool, fullMass Q (x, a, (if a then y1 else y0), y0, y1)) = 0 := by rw [← hcx] simp only [cellMass, armMass, observedMarginal_jointMass, Fintype.sum_bool] simp [hc_tf, hc_tt, hc_ff, hc_ft] ring have hn (a y y0 y1 : Bool) : 0 ≤ fullMass Q (x, a, y, y0, y1) := ENNReal.toReal_nonneg simp only [cellMass, outcomeMean, armMass, observedMarginal_jointMass, Fintype.sum_bool] simp [hc_tf, hc_tt, hc_ff, hc_ft] simp only [Fintype.sum_bool] at htotal simp at htotal have h00 := hn false false false false have h01 := hn false false false true have h10 := hn false true true false have h11 := hn false true true true have ht00 := hn true false false false have ht01 := hn true true false true have ht10 := hn true false true false have ht11 := hn true true true true have hz00 : fullMass Q (x, false, false, false, false) = 0 := by nlinarith [htotal] have hz01 : fullMass Q (x, false, false, false, true) = 0 := by nlinarith [htotal] have hz10 : fullMass Q (x, false, true, true, false) = 0 := by nlinarith [htotal] have hz11 : fullMass Q (x, false, true, true, true) = 0 := by nlinarith [htotal] have hzt00 : fullMass Q (x, true, false, false, false) = 0 := by nlinarith [htotal] have hzt01 : fullMass Q (x, true, true, false, true) = 0 := by nlinarith [htotal] have hzt10 : fullMass Q (x, true, false, true, false) = 0 := by nlinarith [htotal] have hzt11 : fullMass Q (x, true, true, true, true) = 0 := by nlinarith [htotal] simp [hz00, hz01, hz10, hz11, hzt00, hzt01, hzt10, hzt11] · have hcxpos : 0 < cellMass (observedMarginal Q) x := lt_of_le_of_ne (cellMass_mem_unitInterval _ _).1 (Ne.symm hcx) have hprop := hOv x hcxpos have htpos : 0 < armMass (observedMarginal Q) x true := by have hr : 0 < propensity (observedMarginal Q) x := lt_of_lt_of_le heps hprop.1 rw [propensity] at hr rcases (div_pos_iff.mp hr) with h | h · exact h.1 · linarith have hfpos : 0 < armMass (observedMarginal Q) x false := by have hr : propensity (observedMarginal Q) x < 1 := lt_of_le_of_lt hprop.2 (by linarith) rw [propensity, div_lt_one hcxpos] at hr linarith [hcellarm] have he_t0 := hExch x true false true have he_t1 := hExch x true true true have he_f0 := hExch x false true false have he_f1 := hExch x false true true simp only [poAtom, Fintype.sum_bool] at he_t0 he_t1 he_f0 he_f1 simp [hc_tf, hc_tt, hc_ff, hc_ft] at he_t0 he_t1 he_f0 he_f1 have htne : fullMass Q (x, true, true, true, true) + fullMass Q (x, true, true, false, true) + (fullMass Q (x, true, false, true, false) + fullMass Q (x, true, false, false, false)) ≠ 0 := by simpa [armMass, observedMarginal_jointMass, Fintype.sum_bool, hc_tf, hc_tt] using ne_of_gt htpos have hfne : fullMass Q (x, false, true, true, true) + fullMass Q (x, false, true, true, false) + (fullMass Q (x, false, false, false, true) + fullMass Q (x, false, false, false, false)) ≠ 0 := by simpa [armMass, observedMarginal_jointMass, Fintype.sum_bool, hc_ff, hc_ft] using ne_of_gt hfpos simp only [cellMass, outcomeMean, armMass, observedMarginal_jointMass, Fintype.sum_bool] simp [hc_tf, hc_tt, hc_ff, hc_ft] field_simp [htne, hfne] linear_combination (fullMass Q (x, false, true, true, true) + fullMass Q (x, false, true, true, false) + (fullMass Q (x, false, false, false, true) + fullMass Q (x, false, false, false, false))) * (he_t0 + he_t1) - (fullMass Q (x, true, true, true, true) + fullMass Q (x, true, false, true, false) + (fullMass Q (x, true, true, false, true) + fullMass Q (x, true, false, false, false))) * (he_f0 + he_f1)

-- keep: canonical law membership certificate explicitly promised by the F1 plan and public experiment API lemma annotationLaw_mem_annotationExperiment {n m d : Nat} {eps : Real} (P : DiscreteLaw d) (hn : 1 ≤ n) (hP : ModelClass d eps P) : annotationLaw P n m ∈ annotationExperiment n m d eps := by letI : IsProbabilityMeasure (labeledProductLaw P n) := by unfold labeledProductLaw infer_instance letI : IsProbabilityMeasure (auxProductLaw P m) := by unfold auxProductLaw infer_instance refine ⟨hn, hP.alphabet, P, hP, ?_, ?_, ?_⟩ · unfold LabeledIid annotationLaw simp · unfold AuxiliaryIid annotationLaw simp · constructor · unfold annotationLaw infer_instance · unfold annotationLaw simp

lemma minimaxRisk_mem_Icc_zero_one (n m d : Nat) (eps : Real) : minimaxRisk n m d eps ∈ Icc (0 : Real) 1 := by have hnonneg (est : {f : Sample n m d → Real // Measurable f}) : 0 ≤ ⨆ P : ClassLaw d eps, twoSampleMSE (annotationLaw P.1 n m) est.1 (ateFunctional P.1) := by cases isEmpty_or_nonempty (ClassLaw d eps) with | inl hempty => letI := hempty simp | inr hnonempty => letI := hnonempty by_cases hbounded : BddAbove (range (fun P : ClassLaw d eps => twoSampleMSE (annotationLaw P.1 n m) est.1 (ateFunctional P.1))) · have hmse : 0 ≤ twoSampleMSE (annotationLaw (Classical.arbitrary (ClassLaw d eps)).1 n m) est.1 (ateFunctional (Classical.arbitrary (ClassLaw d eps)).1) := by exact integral_nonneg (fun z => sq_nonneg (est.1 z - ateFunctional (Classical.arbitrary (ClassLaw d eps)).1)) exact hmse.trans (le_ciSup hbounded (Classical.arbitrary _)) · rw [show (⨆ P : ClassLaw d eps, twoSampleMSE (annotationLaw P.1 n m) est.1 (ateFunctional P.1)) = sSup ∅ from csSup_of_not_bddAbove hbounded] simp have hb : BddBelow (range (fun est : {f : Sample n m d → Real // Measurable f} => ⨆ P : ClassLaw d eps, twoSampleMSE (annotationLaw P.1 n m) est.1 (ateFunctional P.1))) := by refine ⟨0, ?_⟩ rintro _ ⟨est, rfl⟩ exact hnonneg est letI : Nonempty {f : Sample n m d → Real // Measurable f} := ⟨⟨fun _ => 0, measurable_const⟩⟩ constructor · apply le_ciInf exact hnonneg · have hzero : Measurable (fun _ : Sample n m d => (0 : Real)) := measurable_const refine (ciInf_le hb ⟨fun _ => 0, hzero⟩).trans ?_ cases isEmpty_or_nonempty (ClassLaw d eps) with | inl hempty => letI := hempty simp | inr hnonempty => letI := hnonempty apply ciSup_le intro P have ht := ateFunctional_mem_Icc_neg_one_one P.1 P.2.overlap have hs : ateFunctional P.1 ^ 2 ≤ 1 := (sq_le_one_iff_abs_le_one (ateFunctional P.1)).2 (abs_le.mpr ht) letI : IsProbabilityMeasure (annotationLaw P.1 n m) := by unfold annotationLaw labeledProductLaw auxProductLaw infer_instance simpa [twoSampleMSE] using hs

lemma frontierRate_mem_Ioc_zero_one (n m d : Nat) (hn : 1 ≤ n) : frontierRate n m d ∈ Ioc (0 : Real) 1 := by have hnpos : (0 : Real) < n := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hn) constructor · rw [frontierRate] apply lt_min (by norm_num) have hdim : 0 ≤ (d : Real) ^ 2 / (((n + m : Nat) : Real) ^ 2 * logEN n ^ 2) := by positivity exact lt_of_lt_of_le (one_div_pos.mpr hnpos) (le_add_of_nonneg_right hdim) · exact min_le_left _ _

lemma inv_n_le_frontierRate (n m d : Nat) (hn : 1 ≤ n) : 1 / (n : Real) ≤ frontierRate n m d := by have hnpos : (0 : Real) < n := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hn) rw [frontierRate] apply le_min · rw [div_le_iff₀ hnpos] have hnreal : (1 : Real) ≤ n := by exact_mod_cast hn simpa using hnreal · exact le_add_of_nonneg_right (by positivity)

lemma exists_clipped_knownMarginalEstimator (n d : Nat) (est : KnownSample n d → Real) (hest : Measurable est) : ∃ clipped : {f : KnownSample n d → Real // Measurable f ∧ ∀ z, f z ∈ Icc (-1 : Real) 1}, ∀ z (target : Real), target ∈ Icc (-1 : Real) 1 → (clipped.1 z - target) ^ 2 ≤ (est z - target) ^ 2 := by let hbounds : (-1 : Real) ≤ 1 := by norm_num let clipped : KnownSample n d → Real := fun z => clipAte (est z) have hclipped_measurable : Measurable clipped := by dsimp [clipped, clipAte] fun_prop have hclipped_mem : ∀ z, clipped z ∈ Icc (-1 : Real) 1 := by intro z exact (projIcc (-1 : Real) 1 hbounds (est z)).property refine ⟨⟨clipped, hclipped_measurable, hclipped_mem⟩, ?_⟩ intro z target htarget have habs : |clipped z - target| ≤ |est z - target| := by simpa [clipped, clipAte, Set.coe_projIcc, Set.projIcc_of_mem hbounds htarget] using (Set.abs_projIcc_sub_projIcc (a := (-1 : Real)) (b := 1) (c := est z) (d := target) hbounds) exact sq_le_sq.mpr habs

lemma knownMarginalRisk_mem_Icc_zero_one (n d : Nat) (eps : Real) : knownMarginalRisk n d eps ∈ Icc (0 : Real) 1 := by have hnonneg (est : {f : KnownSample n d → Real // Measurable f ∧ ∀ z, f z ∈ Icc (-1 : Real) 1}) : 0 ≤ ⨆ P : ClassLaw d eps, ∫ x, (est.1 (x, auxTableOf P.1) - ateFunctional P.1) ^ 2 ∂(labeledProductLaw P.1 n) := by cases isEmpty_or_nonempty (ClassLaw d eps) with | inl hempty => letI := hempty simp | inr hnonempty => letI := hnonempty by_cases hbounded : BddAbove (range (fun P : ClassLaw d eps => ∫ x, (est.1 (x, auxTableOf P.1) - ateFunctional P.1) ^ 2 ∂(labeledProductLaw P.1 n))) · have hint : 0 ≤ ∫ x, (est.1 (x, auxTableOf (Classical.arbitrary (ClassLaw d eps)).1) - ateFunctional (Classical.arbitrary (ClassLaw d eps)).1) ^ 2 ∂(labeledProductLaw (Classical.arbitrary (ClassLaw d eps)).1 n) := integral_nonneg (fun x => sq_nonneg _) exact hint.trans (le_ciSup hbounded (Classical.arbitrary _)) · rw [show (⨆ P : ClassLaw d eps, ∫ x, (est.1 (x, auxTableOf P.1) - ateFunctional P.1) ^ 2 ∂(labeledProductLaw P.1 n)) = sSup ∅ from csSup_of_not_bddAbove hbounded] simp have hb : BddBelow (range (fun est : {f : KnownSample n d → Real // Measurable f ∧ ∀ z, f z ∈ Icc (-1 : Real) 1} => ⨆ P : ClassLaw d eps, ∫ x, (est.1 (x, auxTableOf P.1) - ateFunctional P.1) ^ 2 ∂(labeledProductLaw P.1 n))) := by refine ⟨0, ?_⟩ rintro _ ⟨est, rfl⟩ exact hnonneg est let zeroEst : {f : KnownSample n d → Real // Measurable f ∧ ∀ z, f z ∈ Icc (-1 : Real) 1} := ⟨fun _ => 0, measurable_const, by intro z; norm_num⟩ letI : Nonempty {f : KnownSample n d → Real // Measurable f ∧ ∀ z, f z ∈ Icc (-1 : Real) 1} := ⟨zeroEst⟩ constructor · apply le_ciInf exact hnonneg · refine (ciInf_le hb zeroEst).trans ?_ cases isEmpty_or_nonempty (ClassLaw d eps) with | inl hempty => letI := hempty simp | inr hnonempty => letI := hnonempty apply ciSup_le intro P have ht := ateFunctional_mem_Icc_neg_one_one P.1 P.2.overlap have hs : ateFunctional P.1 ^ 2 ≤ 1 := (sq_le_one_iff_abs_le_one (ateFunctional P.1)).2 (abs_le.mpr ht) letI : IsProbabilityMeasure (labeledProductLaw P.1 n) := by unfold labeledProductLaw infer_instance simpa [zeroEst] using hs

lemma finite_alternation_duality {eps : Real} (heps : 0 < eps) (heps2 : eps < 1 / 2) : ∃ gamma c : Real, 0 < gamma ∧ 0 < c ∧ ∀ (L : Nat), 2 ≤ L → ∀ B : Real, 0 < B → let kappa := (1 - 2 * eps) / eps let a := gamma * B / (L : Real) ^ 2 a / kappa ≤ B ∧ Nonempty (FiniteMomentDual L (a / kappa) B a c) := by let kappa := (1 - 2 * eps) / eps let D := kappa / ((1 + kappa) * (2 + kappa)) let gamma := min (kappa / 4) (D * kappa / 32) let c := D / 8 have hkappa : 0 < kappa := by dsimp [kappa] apply div_pos · linarith · exact heps have hD : 0 < D := by dsimp [D] exact div_pos hkappa (mul_pos (by linarith) (by linarith)) have hDlt : D < 1 := by dsimp [D] apply (div_lt_one (mul_pos (by linarith [hkappa]) (by linarith [hkappa]))).2 nlinarith [sq_nonneg kappa] have hgamma : 0 < gamma := by dsimp [gamma] positivity have hc : 0 < c := by dsimp [c] positivity refine ⟨gamma, c, hgamma, hc, ?_⟩ intro L hL B hB dsimp only let a := gamma * B / (L : Real) ^ 2 have hLreal : 0 < (L : Real) := by positivity have ha : 0 < a := by dsimp [a] positivity have hgamma_le : gamma ≤ kappa / 4 := min_le_left _ _ have hLtwo : (2 : Real) ≤ L := by exact_mod_cast hL have hLsq : 4 ≤ (L : Real) ^ 2 := by nlinarith have hLsqpos : 0 < (L : Real) ^ 2 := lt_of_lt_of_le (by norm_num) hLsq have hleft : a / kappa ≤ B := by rw [div_le_iff₀ hkappa] dsimp [a] rw [div_le_iff₀ hLsqpos] have : gamma * B ≤ kappa * B := by gcongr <;> linarith nlinarith [mul_pos hkappa hB] refine ⟨hleft, ?_⟩ have hapos : 0 < a / kappa := div_pos ha hkappa have hleft16 : a / kappa ≤ B / 16 := by rw [div_le_iff₀ hkappa] dsimp [a] rw [div_le_iff₀ hLsqpos] have hgamB : gamma * B ≤ (kappa / 4) * B := by gcongr nlinarith [mul_pos hkappa hB] have hright_strict : a / kappa < B := by linarith let f := Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.rationalTarget a have hpole : -a ∉ Icc (a / kappa) B := by intro h linarith [h.1, hapos] have hf : ContinuousOn f (Icc (a / kappa) B) := continuousOn_rationalTarget hpole obtain ⟨A⟩ := exists_alternationDualCertificate hright_strict hf L let E := bestUniformApproxError f (a / kappa) B L have hE : c ≤ E := by by_contra hnot have hElt : E < c := lt_of_not_ge hnot let p₁ := a / kappa let p₂ := 2 * a / kappa have hp₁pos : 0 < p₁ := by dsimp [p₁]; positivity have hp₁p₂ : p₁ < p₂ := by dsimp [p₁, p₂] calc a / kappa < 2 * (a / kappa) := by linarith [hapos] _ = 2 * a / kappa := by ring have hp₂B : p₂ ≤ B := by dsimp [p₂, a] have hgam : gamma ≤ kappa := hgamma_le.trans (by linarith [hkappa]) have hmul : 2 * gamma * B ≤ 2 * kappa * B := by gcongr field_simp [ne_of_gt hkappa, ne_of_gt hLsqpos] nlinarith [mul_pos hkappa hB] have hp₁mem : p₁ ∈ Icc (a / kappa) B := ⟨le_rfl, hp₁p₂.le.trans hp₂B⟩ have hp₂mem : p₂ ∈ Icc (a / kappa) B := ⟨hp₁p₂.le, hp₂B⟩ have hres (p : Real) (hp : p ∈ Icc (a / kappa) B) : |f p - A.approximant.eval p| ≤ E := by have herr : intervalSupNorm (fun x => f x - A.approximant.eval x) (a / kappa) B = E := by simpa [uniformApproxError, E] using A.approximant_best have hu := (intervalSupNorm_le_iff (hf.sub A.approximant.continuous.continuousOn) hright_strict.le).mp (herr.le) p hp exact hu have hf₁ : f p₁ = 1 / (1 + kappa) := by dsimp [f, p₁, Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.rationalTarget] field_simp [ne_of_gt ha, ne_of_gt hkappa] <;> ring have hf₂ : f p₂ = 2 / (2 + kappa) := by dsimp [f, p₂, Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.rationalTarget] field_simp [ne_of_gt ha, ne_of_gt hkappa] <;> ring have hfdiff : f p₂ - f p₁ = D := by rw [hf₁, hf₂] dsimp [D] field_simp ring have hQdiff : D - 2 * E ≤ A.approximant.eval p₂ - A.approximant.eval p₁ := by have h1 := abs_le.mp (hres p₁ hp₁mem) have h2 := abs_le.mp (hres p₂ hp₂mem) linarith [hfdiff] obtain ⟨z, hz, hzderiv⟩ := exists_hasDerivAt_eq_slope (fun x => A.approximant.eval x) (fun x => A.approximant.derivative.eval x) hp₁p₂ A.approximant.continuous.continuousOn (fun x _ => A.approximant.hasDerivAt x) have hzmem : z ∈ Icc (a / kappa) B := ⟨hp₁mem.1.trans hz.1.le, hz.2.le.trans hp₂B⟩ have hQnorm : intervalSupNorm (fun x => A.approximant.eval x) (a / kappa) B ≤ 1 + E := by apply (intervalSupNorm_le_iff A.approximant.continuous.continuousOn hright_strict.le).2 intro x hx have hr := abs_le.mp (hres x hx) have hfx0 : 0 ≤ f x := by dsimp [f, Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.rationalTarget] exact div_nonneg (hp₁pos.le.trans hx.1) (by linarith [ha, hp₁pos, hx.1]) have hfx1 : f x ≤ 1 := by dsimp [f, Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.rationalTarget] apply (div_le_one (by linarith [ha, hp₁pos, hx.1])).2 linarith [ha] rw [abs_le] constructor <;> linarith have hmarkov := markov_derivative_Icc A.approximant hright_strict L A.approximant_degree have hzupper := (intervalSupNorm_le_iff A.approximant.derivative.continuous.continuousOn hright_strict.le).mp hmarkov z hzmem have hE0 : 0 ≤ E := by exact Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.bestUniformApproxError_nonneg hright_strict hf L have hEone : E < 1 := hElt.trans (by dsimp [c]; linarith [hDlt]) have hden : 0 < B - a / kappa := sub_pos.mpr hright_strict have hslope : (D - 2 * E) / (p₂ - p₁) ≤ |A.approximant.derivative.eval z| := by rw [hzderiv] rw [abs_of_nonneg] · exact div_le_div_of_nonneg_right hQdiff (sub_nonneg.mpr hp₁p₂.le) · apply div_nonneg · dsimp [c] at hElt nlinarith · linarith have hgamma_le' : gamma ≤ D * kappa / 32 := min_le_right _ _ have hhalfden : B / 2 ≤ B - a / kappa := by linarith [hleft16] have hupper : |A.approximant.derivative.eval z| ≤ (2 * (L : Real) ^ 2 / (B - a / kappa)) * (1 + E) := hzupper.trans (mul_le_mul_of_nonneg_left hQnorm (by positivity)) dsimp [p₁, p₂, a] at hslope hupper hhalfden have hupper' : |A.approximant.derivative.eval z| ≤ 8 * (L : Real) ^ 2 / B := by have hfac : 0 ≤ 2 * (L : Real) ^ 2 := by positivity have hdiv : 2 * (L : Real) ^ 2 / (B - a / kappa) ≤ 2 * (L : Real) ^ 2 / (B / 2) := div_le_div_of_nonneg_left hfac (by positivity) hhalfden calc |A.approximant.derivative.eval z| ≤ (2 * (L : Real) ^ 2 / (B - a / kappa)) * (1 + E) := hupper _ ≤ (2 * (L : Real) ^ 2 / (B / 2)) * (1 + E) := mul_le_mul_of_nonneg_right hdiv (by linarith) _ ≤ (2 * (L : Real) ^ 2 / (B / 2)) * 2 := by apply mul_le_mul_of_nonneg_left (by linarith [hEone]) positivity _ = 8 * (L : Real) ^ 2 / B := by field_simp [ne_of_gt hB] ring have hkapne : kappa ≠ 0 := ne_of_gt hkappa have hgamne : gamma ≠ 0 := ne_of_gt hgamma have hBne : B ≠ 0 := ne_of_gt hB have hLne : (L : Real) ^ 2 ≠ 0 := ne_of_gt hLsqpos field_simp [hkapne, hgamne, hBne, hLne] at hslope have hprod : gamma * B * |A.approximant.derivative.eval z| ≤ 8 * gamma * (L : Real) ^ 2 := by calc gamma * B * |A.approximant.derivative.eval z| ≤ gamma * B * (8 * (L : Real) ^ 2 / B) := by gcongr _ = 8 * gamma * (L : Real) ^ 2 := by field_simp [hBne] dsimp [c] at hElt nlinarith [mul_pos hLsqpos hkappa] let sign : Real := if 0 ≤ ∑ i, A.weights i * f (A.nodes i) then 1 else -1 refine ⟨{ node := A.nodes node_injective := A.nodes_strictMono.injective weight := fun i => sign * A.weights i support := A.nodes_mem totalVariation := ?_ moments := ?_ gap := ?_ }⟩ · simp only [abs_mul, Finset.mul_sum] have hsignabs : |sign| = 1 := by dsimp [sign] split <;> simp simpa [hsignabs] using A.weights_normalized · intro j hj simp_rw [mul_assoc] rw [← Finset.mul_sum, A.moments_zero j hj, mul_zero] · have htarget : |∑ i, A.weights i * f (A.nodes i)| = E := by rw [A.target_eq] rcases A.orientation_eq with h | h <;> rw [h] <;> simp [E, abs_of_nonneg (Causalean.Mathlib.Analysis.FinitePolynomialAlternationDuality.bestUniformApproxError_nonneg hright_strict hf L)] change c ≤ ∑ i, sign * A.weights i * (A.nodes i / (A.nodes i + a)) simp_rw [mul_assoc] rw [← Finset.mul_sum] change c ≤ sign * ∑ i, A.weights i * f (A.nodes i) rw [show sign * ∑ i, A.weights i * f (A.nodes i) = |∑ i, A.weights i * f (A.nodes i)| by simp only [sign] split_ifs with h · simpa [abs_of_nonneg h] · have : ∑ i, A.weights i * f (A.nodes i) ≤ 0 := le_of_not_ge h simpa [abs_of_nonpos this]] simpa [htarget] using hE

lemma logEN_pos_of_one_le (n : Nat) (hn : 1 ≤ n) : 0 < logEN n := by rw [logEN] apply Real.log_pos have he : 1 < exp 1 := Real.one_lt_exp_iff.mpr (by norm_num) have hnR : (1 : Real) ≤ n := by exact_mod_cast hn exact he.trans_le (by simpa using mul_le_mul_of_nonneg_left hnR (Real.exp_nonneg 1))

lemma frontierRate_sequence_formula (mSeq dSeq : Nat → Nat) (n : Nat) : frontierRate n (mSeq n) (dSeq n) = min 1 (1 / (n : Real) + ((dSeq n : Real) / (((n + mSeq n : Nat) : Real) * logEN n)) ^ 2) := by rw [frontierRate] simp only [Nat.cast_add, div_pow] ring

lemma annotation_frontier_consistency_iff (mSeq dSeq : Nat → Nat) (_hd : ∀ n, 1 ≤ n → 2 ≤ dSeq n) : Tendsto (fun n ↦ frontierRate n (mSeq n) (dSeq n)) atTop (nhds 0) ↔ Tendsto (fun n ↦ (dSeq n : Real) / (((n + mSeq n : Nat) : Real) * logEN n)) atTop (nhds 0) := by let b : Nat → Real := fun n ↦ (dSeq n : Real) / (((n + mSeq n : Nat) : Real) * logEN n) have hnat : Tendsto (fun n : Nat ↦ (n : Real)) atTop atTop := tendsto_natCast_atTop_atTop have hinv : Tendsto (fun n : Nat ↦ 1 / (n : Real)) atTop (nhds 0) := by simpa [one_div, Function.comp_def] using tendsto_inv_atTop_zero.comp hnat have hb_nonneg : ∀ᶠ n in atTop, 0 ≤ b n := by filter_upwards [eventually_ge_atTop 1] with n hn dsimp [b] exact div_nonneg (Nat.cast_nonneg _) (mul_nonneg (Nat.cast_nonneg _) (logEN_pos_of_one_le n hn).le) constructor · intro hr have hsmall : ∀ᶠ n in atTop, frontierRate n (mSeq n) (dSeq n) < 1 / 2 := (tendsto_order.1 hr).2 (1 / 2) (by norm_num) have hbsq : Tendsto (fun n ↦ (b n) ^ 2) atTop (nhds 0) := by apply squeeze_zero' (g := fun n ↦ frontierRate n (mSeq n) (dSeq n)) · exact Filter.Eventually.of_forall fun n ↦ sq_nonneg (b n) · filter_upwards [eventually_ge_atTop 1, hsmall] with n hn hs rw [frontierRate_sequence_formula] have hsum : 1 / (n : Real) + b n ^ 2 ≤ 1 := by by_contra h rw [frontierRate_sequence_formula, min_eq_left (le_of_not_ge h)] at hs norm_num at hs rw [min_eq_right hsum] exact le_add_of_nonneg_left (by positivity) · exact hr have hsqrt : Tendsto (fun n ↦ sqrt ((b n) ^ 2)) atTop (nhds 0) := by simpa [Function.comp_def] using Real.continuous_sqrt.continuousAt.tendsto.comp hbsq apply (hsqrt.congr' ?_) filter_upwards [hb_nonneg] with n hn rw [Real.sqrt_sq_eq_abs, abs_of_nonneg hn] · intro hb have hb' : Tendsto b atTop (nhds 0) := by simpa [b] using hb have hsum : Tendsto (fun n : Nat ↦ 1 / (n : Real) + b n ^ 2) atTop (nhds 0) := by convert hinv.add (hb'.pow 2) using 1 <;> norm_num have hmin : Tendsto (fun n : Nat ↦ min (1 : Real) (1 / (n : Real) + b n ^ 2)) atTop (nhds 0) := by convert (tendsto_const_nhds.min hsum) using 1 <;> norm_num apply hmin.congr' filter_upwards with n exact (frontierRate_sequence_formula mSeq dSeq n).symm

lemma annotation_frontier_parametric_iff (mSeq dSeq : Nat → Nat) (_hd : ∀ n, 1 ≤ n → 2 ≤ dSeq n) : (fun n ↦ frontierRate n (mSeq n) (dSeq n)) =O[atTop] (fun n ↦ 1 / (n : Real)) ↔ (fun n ↦ (dSeq n : Real)) =O[atTop] (fun n ↦ ((n + mSeq n : Nat) : Real) * logEN n / sqrt n) := by let D : Nat → Real := fun n ↦ ((n + mSeq n : Nat) : Real) * logEN n let b : Nat → Real := fun n ↦ (dSeq n : Real) / D n let inv : Nat → Real := fun n ↦ 1 / (n : Real) let rate : Nat → Real := fun n ↦ frontierRate n (mSeq n) (dSeq n) have hDpos : ∀ᶠ n in atTop, 0 < D n := by filter_upwards [eventually_ge_atTop 1] with n hn dsimp [D] exact mul_pos (by exact_mod_cast (hn.trans (le_add_right n (mSeq n)))) (logEN_pos_of_one_le n hn) have hinv_nonneg : ∀ᶠ n in atTop, 0 ≤ inv n := by filter_upwards [eventually_ge_atTop 1] with n hn dsimp [inv] positivity have hinv_zero : Tendsto inv atTop (nhds 0) := by dsimp [inv] simpa [one_div, Function.comp_def] using tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop have hb_nonneg : ∀ᶠ n in atTop, 0 ≤ b n := by filter_upwards [hDpos] with n hD exact div_nonneg (Nat.cast_nonneg _) hD.le constructor · intro hr have hr' : rate =O[atTop] inv := by simpa [rate, inv] using hr have hrzero := hr'.trans_tendsto hinv_zero have hsmall : ∀ᶠ n in atTop, rate n < 1 / 2 := (tendsto_order.1 hrzero).2 (1 / 2) (by norm_num) have hb_sq_le : (fun n ↦ b n ^ 2) =O[atTop] rate := by apply IsBigO.of_bound 1 filter_upwards [eventually_ge_atTop 1, hsmall] with n hn hs rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _), abs_of_nonneg (frontierRate_mem_Ioc_zero_one _ _ _ hn).1.le, one_mul] have hsum : 1 / (n : Real) + b n ^ 2 ≤ 1 := by by_contra h change frontierRate n (mSeq n) (dSeq n) < 1 / 2 at hs rw [frontierRate_sequence_formula] at hs rw [min_eq_left (le_of_not_ge (by simpa [b, D] using h))] at hs norm_num at hs change b n ^ 2 ≤ frontierRate n (mSeq n) (dSeq n) rw [frontierRate_sequence_formula, min_eq_right (by simpa [b, D] using hsum)] exact le_add_of_nonneg_left (by positivity) have hb2 : (fun n ↦ b n ^ 2) =O[atTop] inv := hb_sq_le.trans hr' have hbsqrt : (fun n ↦ sqrt (b n ^ 2)) =O[atTop] (fun n ↦ sqrt (inv n)) := hb2.sqrt hinv_nonneg have hbO : b =O[atTop] (fun n ↦ sqrt (inv n)) := hbsqrt.congr' (by filter_upwards [hb_nonneg] with n hn rw [Real.sqrt_sq_eq_abs, abs_of_nonneg hn]) Filter.EventuallyEq.rfl have hmul := hbO.mul (isBigO_refl D atTop) apply hmul.congr' · filter_upwards [hDpos] with n hD dsimp [b] field_simp · filter_upwards [eventually_ge_atTop 1] with n hn dsimp [inv, D] rw [Real.sqrt_div (by norm_num : (0 : Real) ≤ 1), Real.sqrt_one] ring · intro hdO have hdiv := hdO.mul (isBigO_refl (fun n ↦ (D n)⁻¹) atTop) have hbO : b =O[atTop] (fun n ↦ 1 / sqrt n) := by apply hdiv.congr' · filter_upwards [hDpos] with n hD dsimp [b] rw [div_eq_mul_inv] · filter_upwards [hDpos, eventually_ge_atTop 1] with n hD hn dsimp [D] dsimp [D] at hD have hlog := logEN_pos_of_one_le n hn field_simp [hD.ne', hlog.ne'] have hb2 := hbO.pow 2 have hb2' : (fun n ↦ b n ^ 2) =O[atTop] inv := by apply hb2.congr' Filter.EventuallyEq.rfl filter_upwards [eventually_ge_atTop 1] with n hn dsimp [inv] have hnR : (0 : Real) < n := by exact_mod_cast hn rw [div_pow, one_pow, Real.sq_sqrt hnR.le] have hsum : (fun n ↦ inv n + b n ^ 2) =O[atTop] inv := (isBigO_refl inv atTop).add hb2' refine (show rate =O[atTop] (fun n ↦ inv n + b n ^ 2) by apply IsBigO.of_bound 1 filter_upwards [eventually_ge_atTop 1] with n hn rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (frontierRate_mem_Ioc_zero_one _ _ _ hn).1.le, abs_of_nonneg (add_nonneg (by dsimp [inv]; positivity) (sq_nonneg _)), one_mul] rw [frontierRate_sequence_formula] exact min_le_right _ _).trans hsum

lemma coefficientL1_chebG_le (L : Nat) (hL : 0 < L) : coefficientL1 (chebG L) ≤ (6 : Real) ^ L := by rw [chebG_eq_explicit L hL] calc coefficientL1 (explicitG L) = ∑ j ∈ (explicitG L).support, |(explicitG L).coeff j| := rfl _ ≤ ∑ j ∈ range (L - 1), |(explicitG L).coeff j| := by apply Finset.sum_le_sum_of_subset_of_nonneg (explicitG_support_subset L) intro j _ _ exact abs_nonneg _ _ = DiscreteAteMinimaxLoggap.gpos L 1 := by unfold DiscreteAteMinimaxLoggap.gpos apply Finset.sum_congr rfl intro j hj simp [explicitG, Finset.mem_range.mp hj] _ ≤ (6 : Real) ^ L := by simpa using DiscreteAteMinimaxLoggap.gpos_bound hL (z := (1 : Real)) (by norm_num)

lemma explicit_chebyshev_calibration (L : Nat) (hL : 2 ≤ L) : ChebyshevCalibration L := by have hLpos : 0 < L := by omega refine ⟨coefficientL1_chebQ_le L hLpos, ?_, ?_, ?_⟩ · have hg := coefficientL1_chebG_le L hLpos have hpow : (6 : Real) ^ L ≤ 7 ^ L := pow_le_pow_left₀ (by norm_num) (by norm_num) L have htwo : (2 : Real) ≤ 2 ^ L := by calc (2 : Real) = 2 ^ (1 : Nat) := by norm_num _ ≤ 2 ^ L := pow_le_pow_right₀ (by norm_num) (by omega) calc 2 * coefficientL1 (chebG L) ≤ 2 * 6 ^ L := by gcongr _ ≤ 2 ^ L * 7 ^ L := mul_le_mul htwo hpow (by positivity) (by positivity) _ = 14 ^ L := by rw [← mul_pow]; norm_num · intro a t B s0 s1 ht hB hs0 hs1 hLD dsimp only let D := t * B let p := s0 + s1 let q := 1 + p / B have hD : 0 < D := mul_pos ht hB have hrate0 : D * (s0 / B) = t * s0 := by dsimp [D] field_simp have hrate1 : D * (s1 / B) = t * s1 := by dsimp [D] field_simp have hsupp : (chebG L).support ⊆ range (L - 1) := by rw [chebG_eq_explicit L hLpos] exact explicitG_support_subset L let Xj : Nat → Nat × Nat → Real := fun j K ↦ sameArmMonomial a (j + 1) D K + crossArmMonomial a j D K let μ := (poissonMeasure (toNNReal (D * (s0 / B)))).prod (poissonMeasure (toNNReal (D * (s1 / B)))) have hjOrder (j : Nat) (hj : j ∈ (chebG L).support) : j + 1 ≤ L := by have hjr := Finset.mem_range.mp (hsupp hj) omega have hXmem (j : Nat) (hj : j ∈ (chebG L).support) : MemLp (Xj j) 2 μ := by exact armMonomial_sum_memLp a j (D := D) (z0 := s0 / B) (z1 := s1 / B) hD have hXsq (j : Nat) (hj : j ∈ (chebG L).support) : (∫ K, Xj j K ^ 2 ∂μ) ≤ ((6 : Real) ^ L * q ^ L) ^ 2 := by have h := armMonomial_sum_sq_le a hD hB hs0 hs1 hLD (hjOrder j hj) dsimp [Xj, μ, q, p] at h ⊢ calc _ ≤ (36 : Real) ^ L * (1 + (s0 + s1) / B) ^ (2 * L) := h _ = ((6 : Real) ^ L * (1 + (s0 + s1) / B) ^ L) ^ 2 := by rw [show (36 : Real) = 6 * 6 by norm_num, mul_pow] rw [show 2 * L = L + L by omega, pow_add, mul_pow, pow_two] ring have houter := DiscreteOptimalValueMinimaxMatched.integral_sq_finset_sum_le_coeffL1 μ (chebG L).support (chebG L).coeff Xj ((6 : Real) ^ L * q ^ L) (by positivity) hXmem hXsq have hlift : (fun K : Nat × Nat ↦ factorialLift a L B t K.1 K.2) = fun K ↦ ∑ j ∈ (chebG L).support, (chebG L).coeff j * Xj j K := by funext K unfold factorialLift apply Finset.sum_congr rfl intro j hj dsimp [Xj, D, sameArmMonomial, crossArmMonomial] cases a <;> simp only [Bool.false_eq_true, ↓reduceIte] <;> ring have hmoment : factorialLiftSecondMoment a L B t s0 s1 ≤ coefficientL1 (chebG L) ^ 2 * ((6 : Real) ^ L * q ^ L) ^ 2 := by unfold factorialLiftSecondMoment dsimp [μ] at houter rw [hrate0, hrate1] at houter rw [show (fun K : Nat × Nat ↦ factorialLift a L B t K.1 K.2 ^ 2) = (fun K ↦ (∑ j ∈ (chebG L).support, (chebG L).coeff j * Xj j K) ^ 2) by funext K rw [congrFun hlift K]] simpa only [coefficientL1] using houter have hg := coefficientL1_chebG_le L hLpos have hq0 : 0 ≤ q := by dsimp [q, p] have := div_nonneg (add_nonneg hs0 hs1) hB.le linarith have hg0 : 0 ≤ coefficientL1 (chebG L) := by unfold coefficientL1 exact Finset.sum_nonneg fun _ _ ↦ abs_nonneg _ have hmain : factorialLiftSecondMoment a L B t s0 s1 ≤ (1296 : Real) ^ L * q ^ (2 * L) := by calc _ ≤ coefficientL1 (chebG L) ^ 2 * ((6 : Real) ^ L * q ^ L) ^ 2 := hmoment _ ≤ ((6 : Real) ^ L) ^ 2 * ((6 : Real) ^ L * q ^ L) ^ 2 := by exact mul_le_mul_of_nonneg_right (pow_le_pow_left₀ hg0 hg 2) (sq_nonneg _) _ = (1296 : Real) ^ L * q ^ (2 * L) := by norm_num [pow_two, pow_mul, Nat.mul_comm] rw [show (1296 : Real) = 6 * 6 * 6 * 6 by norm_num, mul_pow, mul_pow, mul_pow] ring constructor · dsimp [p, q] at hmain ⊢ exact hmain.trans (mul_le_mul_of_nonneg_right (pow_le_pow_left₀ (by norm_num) (by norm_num : (1296 : Real) ≤ 7056) L) (by positivity)) · intro hpB have hq2 : q ≤ 2 := by dsimp [q, p] have : (s0 + s1) / B ≤ 1 := (div_le_one hB).2 hpB linarith calc factorialLiftSecondMoment a L B t s0 s1 ≤ (1296 : Real) ^ L * q ^ (2 * L) := hmain _ ≤ (1296 : Real) ^ L * 2 ^ (2 * L) := by gcongr _ = (5184 : Real) ^ L := by rw [show (5184 : Real) = 1296 * 4 by norm_num, mul_pow, show (2 : Real) ^ (2 * L) = 4 ^ L by rw [show (4 : Real) = 2 ^ 2 by norm_num, pow_mul]] _ ≤ (7056 : Real) ^ L := pow_le_pow_left₀ (by norm_num) (by norm_num) L · intro z hz rcases chebE_interval_bounds L hLpos hz with ⟨h0, h1, hinv⟩ exact ⟨h0, h1, hinv, chebG_defining_identity L hLpos z⟩

lemma commonMarginal_logEN_pos (n : Nat) (hn : 1 ≤ n) : 0 < logEN n := by rw [logEN] apply Real.log_pos have he : 1 < exp 1 := Real.one_lt_exp_iff.mpr (by norm_num) have hnR : (1 : Real) ≤ n := by exact_mod_cast hn nlinarith

lemma commonMarginal_one_le_logEN (n : Nat) (hn : 1 ≤ n) : 1 ≤ logEN n := by have hnR : (0 : Real) < n := by exact_mod_cast hn have hlog : 0 ≤ log (n : Real) := Real.log_nonneg (by exact_mod_cast hn) rw [logEN, Real.log_mul (Real.exp_ne_zero 1) hnR.ne', Real.log_exp] linarith

lemma commonMarginal_logEN_le_two_sqrt (n : Nat) (hn : 1 ≤ n) : logEN n ≤ 2 * sqrt n := by have hnR : (0 : Real) < n := by exact_mod_cast hn have hs : 1 ≤ sqrt (n : Real) := Real.one_le_sqrt.mpr (by exact_mod_cast hn) have hlog := Real.log_le_sub_one_of_pos (Real.sqrt_pos.2 hnR) rw [Real.log_sqrt hnR.le] at hlog rw [logEN, Real.log_mul (Real.exp_ne_zero 1) hnR.ne', Real.log_exp] nlinarith

lemma commonMarginal_logEN_le_nat (n : Nat) (hn : 1 ≤ n) : logEN n ≤ n := by have hnR : (0 : Real) < n := by exact_mod_cast hn have hlog := Real.log_le_sub_one_of_pos hnR rw [logEN, Real.log_mul (Real.exp_ne_zero 1) hnR.ne', Real.log_exp] linarith

lemma commonMarginal_half_le_floor {x : Real} (hx : 1 ≤ x) : x / 2 ≤ (Nat.floor x : Real) := by by_cases hx2 : x ≤ 2 · have hfloor : 1 ≤ Nat.floor x := Nat.le_floor (by simpa using hx) have hfloorR : (1 : Real) ≤ Nat.floor x := by exact_mod_cast hfloor linarith · have hfloor := Nat.sub_one_lt_floor x linarith

lemma commonMarginal_degree_upper {eps : Real} (calibration : CommonMarginalCalibration eps) (n L : Nat) (hn : 1 ≤ n) (hL : L = ceil (calibration.degreeConstant * logEN n)) : (L : Real) ≤ (calibration.degreeConstant + 1) * logEN n := by have hlog := commonMarginal_one_le_logEN n hn have hx : 0 ≤ calibration.degreeConstant * logEN n := mul_nonneg calibration.degreeConstant_pos.le (by linarith) have hc := Nat.ceil_lt_add_one hx rw [← hL] at hc nlinarith

lemma commonMarginal_degree_lower {eps : Real} {calibration : CommonMarginalCalibration eps} {C rho : Real} (closure : CommonMarginalCalibrationClosure calibration C rho) (n L : Nat) (hn : 1 ≤ n) (hL : L = ceil (calibration.degreeConstant * logEN n)) : 2 ≤ L := by have hlog := commonMarginal_one_le_logEN n hn have hx : (2 : Real) ≤ calibration.degreeConstant * logEN n := by have hm := mul_le_mul_of_nonneg_left hlog calibration.degreeConstant_pos.le have hm' : calibration.degreeConstant ≤ calibration.degreeConstant * logEN n := by simpa only [mul_one] using hm exact closure.degreeFloor.trans hm' rw [hL] exact_mod_cast (hx.trans (Nat.le_ceil _))

lemma commonMarginal_rareCount_degree_lower {eps : Real} {calibration : CommonMarginalCalibration eps} {C rho : Real} (hC : 0 < C) (closure : CommonMarginalCalibrationClosure calibration C rho) (n m d L k : Nat) (hn : 1 ≤ n) (hd : 2 ≤ d) (hL : L = ceil (calibration.degreeConstant * logEN n)) (hk : k = min (d - 1) ⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊) (hnon : ¬commonMarginalParametricRegime calibration n m d) : (L : Real) ^ 2 / ((1 / (65536 * C)) * calibration.dualGap ^ 2 * calibration.gamma) ≤ k := by let K : Real := (1 / (65536 * C)) * calibration.dualGap ^ 2 * calibration.gamma let N : Real := (n + m : Nat) let ell : Real := logEN n have hK : 0 < K := by dsimp [K] exact mul_pos (mul_pos (div_pos (by norm_num) (mul_pos (by norm_num) hC)) (sq_pos_of_pos calibration.dualGap_pos)) calibration.gamma_pos have hnR : (0 : Real) < n := by exact_mod_cast hn have hN : (0 : Real) < N := by dsimp [N]; positivity have hNn : (n : Real) ≤ N := by dsimp [N] exact_mod_cast Nat.le_add_right n m have hell : 0 < ell := by exact commonMarginal_logEN_pos n hn have hLtwo := commonMarginal_degree_lower closure n L hn hL have hLpos : (0 : Real) < L := by exact_mod_cast (lt_of_lt_of_le (by omega : 0 < 2) hLtwo) have hLupper : (L : Real) ≤ (calibration.degreeConstant + 1) * ell := by exact commonMarginal_degree_upper calibration n L hn hL have hellN : ell ≤ N := (commonMarginal_logEN_le_nat n hn).trans hNn have hrK : 4 * (calibration.degreeConstant + 1) / K ≤ calibration.rareCountConstant := by simpa [K] using closure.rareCountLower have hxone : 1 ≤ calibration.rareCountConstant * N * L := by have hr : (4 : Real) ≤ calibration.rareCountConstant := closure.rareCountFloor have hN1 : (1 : Real) ≤ N := by dsimp [N] exact_mod_cast (show 1 ≤ n + m by omega) have hrN : (4 : Real) ≤ calibration.rareCountConstant * N := by nlinarith [mul_le_mul hr hN1 (by norm_num : (0 : Real) ≤ 1) calibration.rareCountConstant_pos.le] have hL1 : (1 : Real) ≤ L := by exact_mod_cast (show 1 ≤ L by omega) have hm := mul_le_mul_of_nonneg_right hrN (by positivity : (0 : Real) ≤ L) nlinarith have hfloorHalf : calibration.rareCountConstant * N * L / 2 ≤ (⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊ : Real) := by simpa [N] using commonMarginal_half_le_floor hxone subst k by_cases hcap : d - 1 ≤ ⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊ · rw [min_eq_left hcap] have hkcast : ((d - 1 : Nat) : Real) = (d : Real) - 1 := by rw [Nat.cast_sub (by omega)] norm_num have hdR : (2 : Real) ≤ d := by exact_mod_cast hd have hkhalf : (d : Real) / 2 ≤ (d - 1 : Nat) := by rw [hkcast] linarith have hreg : calibration.regimeConstant / (n : Real) < (d : Real) ^ 2 / (N ^ 2 * ell ^ 2) := by have h := lt_of_not_ge hnon exact lt_of_lt_of_le h (min_le_right _ _) have hq : (4 * (calibration.degreeConstant + 1) ^ 2 / K) ^ 2 ≤ calibration.regimeConstant := by simpa [K] using closure.regimeScale have hlogSqrt := commonMarginal_logEN_le_two_sqrt n hn have hsqrt : 0 < sqrt (n : Real) := Real.sqrt_pos.2 hnR have hsqrtSq : sqrt (n : Real) ^ 2 = n := Real.sq_sqrt hnR.le have hcross : (4 * (calibration.degreeConstant + 1) ^ 2 / K * N * ell) ^ 2 < ((d : Real) * sqrt n) ^ 2 := by have hden2 : 0 < N ^ 2 * ell ^ 2 := mul_pos (sq_pos_of_pos hN) (sq_pos_of_pos hell) rw [div_lt_div_iff₀ hnR hden2] at hreg nlinarith [mul_nonneg (sq_nonneg N) (sq_nonneg ell), hq] have hcross' : 4 * (calibration.degreeConstant + 1) ^ 2 / K * N * ell < (d : Real) * sqrt n := by have hl0 : 0 ≤ 4 * (calibration.degreeConstant + 1) ^ 2 / K * N * ell := by positivity have hr0 : 0 ≤ (d : Real) * sqrt n := by positivity exact (sq_lt_sq₀ hl0 hr0).mp hcross have htarget : 2 * (L : Real) ^ 2 / K ≤ d := by have hellS : ell * sqrt n ≤ 2 * n := by nlinarith have hLN : ell * sqrt n ≤ 2 * N := hellS.trans (by nlinarith) have hLU : (L : Real) ^ 2 ≤ (calibration.degreeConstant + 1) ^ 2 * ell ^ 2 := by nlinarith [sq_nonneg ((calibration.degreeConstant + 1) * ell - (L : Real))] have hD1 : 0 < calibration.degreeConstant + 1 := by linarith [calibration.degreeConstant_pos] have hmul := mul_le_mul_of_nonneg_left hLN (mul_nonneg (mul_nonneg (by positivity : (0 : Real) ≤ 2) (sq_nonneg (calibration.degreeConstant + 1))) hell.le) have hcrossK : 4 * (calibration.degreeConstant + 1) ^ 2 * N * ell < (d : Real) * sqrt n * K := by have := mul_lt_mul_of_pos_right hcross' hK field_simp [ne_of_gt hK] at this simpa only [mul_assoc, mul_comm, mul_left_comm] using this have hLs : 2 * (L : Real) ^ 2 * sqrt n ≤ 4 * (calibration.degreeConstant + 1) ^ 2 * N * ell := by nlinarith [mul_nonneg (sq_nonneg (L : Real)) hsqrt.le] have hLK : 2 * (L : Real) ^ 2 * sqrt n < (d : Real) * sqrt n * K := hLs.trans_lt hcrossK have hLK' : (2 * (L : Real) ^ 2) * sqrt n < ((d : Real) * K) * sqrt n := by convert hLK using 1 <;> ring have := lt_of_mul_lt_mul_right hLK' hsqrt.le exact le_of_lt ((div_lt_iff₀ hK).2 (by nlinarith [this])) change (L : Real) ^ 2 / K ≤ ((d - 1 : Nat) : Real) calc (L : Real) ^ 2 / K ≤ (d : Real) / 2 := by have ht' : 2 * ((L : Real) ^ 2 / K) ≤ (d : Real) := by calc 2 * ((L : Real) ^ 2 / K) = 2 * (L : Real) ^ 2 / K := by ring _ ≤ (d : Real) := htarget calc (L : Real) ^ 2 / K = (2 * ((L : Real) ^ 2 / K)) / 2 := by ring _ ≤ (d : Real) / 2 := div_le_div_of_nonneg_right ht' (by norm_num) _ ≤ ((d - 1 : Nat) : Real) := hkhalf · rw [min_eq_right (Nat.le_of_not_ge hcap)] have hscale : (L : Real) ^ 2 / K ≤ calibration.rareCountConstant * N * L / 2 := by have hrare : 4 * (calibration.degreeConstant + 1) / K * N ≤ calibration.rareCountConstant * N := mul_le_mul_of_nonneg_right hrK hN.le have hLN : (L : Real) ≤ (calibration.degreeConstant + 1) * N := hLupper.trans (mul_le_mul_of_nonneg_left hellN (by linarith [calibration.degreeConstant_pos])) have hrare' : 4 * (calibration.degreeConstant + 1) * N / K ≤ calibration.rareCountConstant * N := by convert hrare using 1 <;> ring have htwo : 2 * (L : Real) / K ≤ calibration.rareCountConstant * N := by have hLK : 2 * (L : Real) ≤ 4 * (calibration.degreeConstant + 1) * N := by nlinarith have := (div_le_div_iff_of_pos_right hK).2 hLK exact this.trans hrare' have hm := mul_le_mul_of_nonneg_right htwo hLpos.le calc (L : Real) ^ 2 / K = (2 * (L : Real) / K * L) / 2 := by ring _ ≤ (calibration.rareCountConstant * N * L) / 2 := div_le_div_of_nonneg_right hm (by norm_num) exact hscale.trans hfloorHalf

lemma commonMarginal_dimension_absorption {eps : Real} {calibration : CommonMarginalCalibration eps} {C rho : Real} (closure : CommonMarginalCalibrationClosure calibration C rho) (n m d L k : Nat) (hn : 1 ≤ n) (hd : 2 ≤ d) (hL : L = ceil (calibration.degreeConstant * logEN n)) (hk : k = min (d - 1) ⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊) (a : Real) (ha : a = calibration.gamma * (calibration.bandwidthConstant * L / (n + m : Nat)) / (L : Real) ^ 2) : calibration.dimensionConstant * commonMarginalDimensionTerm n m d ≤ (calibration.dualGap * k * a) ^ 2 := by let N : Real := (n + m : Nat) let ell : Real := logEN n have hN : 0 < N := by dsimp [N]; positivity have hell : 0 < ell := commonMarginal_logEN_pos n hn have hLtwo := commonMarginal_degree_lower closure n L hn hL have hLpos : (0 : Real) < L := by exact_mod_cast (show 0 < L by omega) have hLupper := commonMarginal_degree_upper calibration n L hn hL have hxone : 1 ≤ calibration.rareCountConstant * N * L := by have hr := closure.rareCountFloor have hN1 : (1 : Real) ≤ N := by dsimp [N] exact_mod_cast (show 1 ≤ n + m by omega) have hrN : (4 : Real) ≤ calibration.rareCountConstant * N := by nlinarith [mul_le_mul hr hN1 (by norm_num : (0 : Real) ≤ 1) calibration.rareCountConstant_pos.le] have hL1 : (1 : Real) ≤ L := by exact_mod_cast (show 1 ≤ L by omega) have hm := mul_le_mul_of_nonneg_right hrN (by positivity : (0 : Real) ≤ L) nlinarith have hfloorHalf : calibration.rareCountConstant * N * L / 2 ≤ (⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊ : Real) := by simpa [N] using commonMarginal_half_le_floor hxone have ha' : a = calibration.gamma * calibration.bandwidthConstant / (N * L) := by rw [ha] dsimp [N] field_simp [ne_of_gt hLpos, ne_of_gt hN] subst k by_cases hcap : d - 1 ≤ ⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊ · rw [min_eq_left hcap] have hkcast : ((d - 1 : Nat) : Real) = (d : Real) - 1 := by rw [Nat.cast_sub (by omega)] norm_num have hdR : (2 : Real) ≤ d := by exact_mod_cast hd have hkhalf : (d : Real) / 2 ≤ (d - 1 : Nat) := by rw [hkcast] linarith have hterm : commonMarginalDimensionTerm n m d ≤ (d : Real) ^ 2 / (N ^ 2 * ell ^ 2) := by exact min_le_right _ _ have hdim := closure.dimensionBranch rw [ha'] have hD1 : 0 < calibration.degreeConstant + 1 := by linarith [calibration.degreeConstant_pos] have hdim0 : 0 ≤ calibration.dimensionConstant := calibration.dimensionConstant_pos.le have hterm0 : 0 ≤ commonMarginalDimensionTerm n m d := by unfold commonMarginalDimensionTerm positivity calc calibration.dimensionConstant * commonMarginalDimensionTerm n m d ≤ calibration.dimensionConstant * ((d : Real) ^ 2 / (N ^ 2 * ell ^ 2)) := mul_le_mul_of_nonneg_left hterm hdim0 _ ≤ (calibration.dualGap * calibration.gamma * calibration.bandwidthConstant / (2 * (calibration.degreeConstant + 1))) ^ 2 * ((d : Real) ^ 2 / (N ^ 2 * ell ^ 2)) := mul_le_mul_of_nonneg_right hdim (div_nonneg (sq_nonneg _) (mul_nonneg (sq_nonneg _) (sq_nonneg _))) _ ≤ (calibration.dualGap * (d - 1 : Nat) * (calibration.gamma * calibration.bandwidthConstant / (N * L))) ^ 2 := by have hdle : (d : Real) ≤ 2 * ((d - 1 : Nat) : Real) := by nlinarith [hkhalf] have hbase : calibration.dualGap * calibration.gamma * calibration.bandwidthConstant * (d : Real) / (2 * (calibration.degreeConstant + 1) * N * ell) ≤ calibration.dualGap * ((d - 1 : Nat) : Real) * (calibration.gamma * calibration.bandwidthConstant / (N * L)) := by rw [show calibration.dualGap * calibration.gamma * calibration.bandwidthConstant * (d : Real) / (2 * (calibration.degreeConstant + 1) * N * ell) = (calibration.dualGap * calibration.gamma * calibration.bandwidthConstant * (d : Real)) / ((2 * (calibration.degreeConstant + 1)) * (N * ell)) by ring, show calibration.dualGap * ((d - 1 : Nat) : Real) * (calibration.gamma * calibration.bandwidthConstant / (N * L)) = (calibration.dualGap * ((d - 1 : Nat) : Real) * (calibration.gamma * calibration.bandwidthConstant)) / (N * L) by ring] apply (div_le_div_iff₀ (show 0 < (2 * (calibration.degreeConstant + 1)) * (N * ell) by exact mul_pos (mul_pos (by norm_num) hD1) (mul_pos hN hell)) (mul_pos hN hLpos)).2 have hcore : (d : Real) * L ≤ (2 * ((d - 1 : Nat) : Real)) * ((calibration.degreeConstant + 1) * ell) := mul_le_mul hdle hLupper (Nat.cast_nonneg _) (by positivity) have hm := mul_le_mul_of_nonneg_left hcore (mul_nonneg (mul_nonneg calibration.dualGap_pos.le calibration.gamma_pos.le) calibration.bandwidthConstant_pos.le) nlinarith have hbase0 : 0 ≤ calibration.dualGap * calibration.gamma * calibration.bandwidthConstant * (d : Real) / (2 * (calibration.degreeConstant + 1) * N * ell) := by exact div_nonneg (mul_nonneg (mul_nonneg (mul_nonneg calibration.dualGap_pos.le calibration.gamma_pos.le) calibration.bandwidthConstant_pos.le) (Nat.cast_nonneg _)) (mul_nonneg (mul_nonneg (mul_nonneg (by norm_num : (0 : Real) ≤ 2) hD1.le) hN.le) hell.le) have hbaseR0 : 0 ≤ calibration.dualGap * ((d - 1 : Nat) : Real) * (calibration.gamma * calibration.bandwidthConstant / (N * L)) := by exact mul_nonneg (mul_nonneg calibration.dualGap_pos.le (Nat.cast_nonneg _)) (div_nonneg (mul_nonneg calibration.gamma_pos.le calibration.bandwidthConstant_pos.le) (mul_nonneg hN.le hLpos.le)) have hs := (sq_le_sq₀ hbase0 hbaseR0).2 hbase calc (calibration.dualGap * calibration.gamma * calibration.bandwidthConstant / (2 * (calibration.degreeConstant + 1))) ^ 2 * ((d : Real) ^ 2 / (N ^ 2 * ell ^ 2)) = (calibration.dualGap * calibration.gamma * calibration.bandwidthConstant * (d : Real) / (2 * (calibration.degreeConstant + 1) * N * ell)) ^ 2 := by field_simp [ne_of_gt hN, ne_of_gt hell, ne_of_gt hD1] _ ≤ _ := hs · rw [min_eq_right (Nat.le_of_not_ge hcap), ha'] have hgap : calibration.dualGap ^ 2 / 4 ≤ calibration.dualGap * (⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊ : Real) * (calibration.gamma * calibration.bandwidthConstant / (N * L)) := by rw [closure.rareCountIdentity] rw [closure.rareCountIdentity] at hfloorHalf have hgp := calibration.gamma_pos have hbp := calibration.bandwidthConstant_pos let t : Real := 2 * calibration.dualGap * calibration.gamma * calibration.bandwidthConstant / (N * L) have ht : 0 ≤ t := by dsimp [t] exact div_nonneg (mul_nonneg (mul_nonneg (mul_nonneg (by norm_num : (0 : Real) ≤ 2) calibration.dualGap_pos.le) calibration.gamma_pos.le) calibration.bandwidthConstant_pos.le) (mul_nonneg hN.le hLpos.le) have hm := mul_le_mul_of_nonneg_right hfloorHalf ht dsimp [t] at hm field_simp [ne_of_gt hN, ne_of_gt hLpos, ne_of_gt hgp, ne_of_gt hbp, ne_of_gt calibration.dualGap_pos] at hm ⊢ nlinarith have hgap0 : 0 ≤ calibration.dualGap ^ 2 / 4 := by positivity have hright0 : 0 ≤ calibration.dualGap * (⌊calibration.rareCountConstant * (n + m : Nat) * L⌋₊ : Real) * (calibration.gamma * calibration.bandwidthConstant / (N * L)) := by exact mul_nonneg (mul_nonneg calibration.dualGap_pos.le (Nat.cast_nonneg _)) (div_nonneg (mul_nonneg calibration.gamma_pos.le calibration.bandwidthConstant_pos.le) (mul_nonneg hN.le hLpos.le)) have hsquare := (sq_le_sq₀ hgap0 hright0).2 hgap have hterm : commonMarginalDimensionTerm n m d ≤ 1 := min_le_left _ _ calc calibration.dimensionConstant * commonMarginalDimensionTerm n m d ≤ calibration.dimensionConstant * 1 := mul_le_mul_of_nonneg_left hterm calibration.dimensionConstant_pos.le _ ≤ calibration.dualGap ^ 4 / 16 := by simpa using closure.dimensionRare _ = (calibration.dualGap ^ 2 / 4) ^ 2 := by ring _ ≤ _ := hsquare

lemma measurable_comp_of_finite_range {alpha beta gamma : Type*} [MeasurableSpace alpha] [MeasurableSpace beta] [MeasurableSpace gamma] [MeasurableSingletonClass beta] {q : alpha → beta} (hq : Measurable q) (hfinite : (Set.range q).Finite) (f : beta → gamma) : Measurable (f ∘ q) := by intro s _ let t := f ⁻¹' s ∩ Set.range q have ht : t.Finite := hfinite.subset (Set.inter_subset_right) have htmeas : MeasurableSet t := ht.measurableSet have hpre := hq htmeas convert hpre using 1 ext x simp [t]

lemma commonMarginalRareCell_injective {k d : Nat} (hkd : k + 1 ≤ d) : Injective (commonMarginalRareCell hkd) := by intro i j hij apply Fin.ext simpa [commonMarginalRareCell] using congrArg val hij

lemma commonMarginalReservoir_ne_rareCell {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (i : Fin k) : commonMarginalReservoir hd ≠ commonMarginalRareCell hkd i := by intro h have := congrArg val h simp [commonMarginalReservoir, commonMarginalRareCell] at this

lemma commonMarginalRawMass_reservoir {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (reservoirMass : Real) (w : Fin k → Real) : commonMarginalRawMass hd hkd reservoirMass w (commonMarginalReservoir hd) = reservoirMass := by simp [commonMarginalRawMass, commonMarginalReservoir_ne_rareCell]

lemma commonMarginalRawMass_rare {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (reservoirMass : Real) (w : Fin k → Real) (i : Fin k) : commonMarginalRawMass hd hkd reservoirMass w (commonMarginalRareCell hkd i) = w i := by rw [commonMarginalRawMass] simp only [if_neg (commonMarginalReservoir_ne_rareCell hd hkd i).symm, zero_add] rw [Finset.sum_eq_single i] · simp · intro j _ hji simp [(commonMarginalRareCell_injective hkd).ne hji |>.symm] · simp

lemma commonMarginalPropensity_rare {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (eps a : Real) (w : Fin k → Real) (i : Fin k) (hi : w i ≠ 0) : commonMarginalPropensity hd hkd eps a w (commonMarginalRareCell hkd i) = eps * (w i + a) / w i := by rw [commonMarginalPropensity] simp only [if_neg (commonMarginalReservoir_ne_rareCell hd hkd i).symm] rw [commonMarginalRawMass_rare hd hkd 0 w i, if_neg hi]

lemma commonMarginalOutcomeMean_rare {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (sign : Real → Real) (branch : Bool) (w : Fin k → Real) (i : Fin k) (hi : w i ≠ 0) : commonMarginalOutcomeMean hd hkd sign branch w (commonMarginalRareCell hkd i) = (1 + (if branch then sign (w i) else -sign (w i))) / 2 := by rw [commonMarginalOutcomeMean, Finset.sum_eq_single i] · simp [hi] · intro j _ hji have hne := (commonMarginalRareCell_injective hkd).ne hji simp [hne.symm] · simp

lemma commonMarginalOutcomeMean_mem {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (sign : Real → Real) (hsign : ∀ p, sign p ∈ Icc (-1 : Real) 1) (branch : Bool) (w : Fin k → Real) (x : Fin d) : commonMarginalOutcomeMean hd hkd sign branch w x ∈ Icc (0 : Real) 1 := by by_cases hx : ∃ i, x = commonMarginalRareCell hkd i ∧ w i ≠ 0 · obtain ⟨i, hxi, hi⟩ := hx rw [hxi, commonMarginalOutcomeMean_rare hd hkd sign branch w i hi] cases branch <;> simp only [Bool.false_eq_true, if_false, if_true] · constructor <;> linarith [(hsign (w i)).1, (hsign (w i)).2] · constructor <;> linarith [(hsign (w i)).1, (hsign (w i)).2] · simp only [commonMarginalOutcomeMean] have hzero : (∑ i, if x = commonMarginalRareCell hkd i ∧ w i ≠ 0 then (1 + (if branch then sign (w i) else -sign (w i))) / 2 else 0) = 0 := by apply Finset.sum_eq_zero intro i _ rw [if_neg (fun hi => hx ⟨i, hi⟩)] rw [hzero] exact ⟨le_rfl, zero_le_one⟩

lemma commonMarginalRawMass_unused {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (reservoirMass : Real) (w : Fin k → Real) (x : Fin d) (hx : x ≠ commonMarginalReservoir hd) (hxi : ∀ i, x ≠ commonMarginalRareCell hkd i) : commonMarginalRawMass hd hkd reservoirMass w x = 0 := by simp [commonMarginalRawMass, hx, hxi]

lemma commonMarginalRawMass_sum {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (reservoirMass : Real) (w : Fin k → Real) : ∑ x, commonMarginalRawMass hd hkd reservoirMass w x = reservoirMass + ∑ i, w i := by simp_rw [commonMarginalRawMass] rw [Finset.sum_add_distrib] rw [Finset.sum_ite_eq'] simp only [Finset.mem_univ, if_true] rw [Finset.sum_comm] apply congrArg (fun z => reservoirMass + z) apply Finset.sum_congr rfl intro i _ rw [Finset.sum_ite_eq'] simp

lemma commonMarginalRawMass_nonneg {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) {reservoirMass : Real} {w : Fin k → Real} (hr : 0 ≤ reservoirMass) (hw : ∀ i, 0 ≤ w i) (x : Fin d) : 0 ≤ commonMarginalRawMass hd hkd reservoirMass w x := by unfold commonMarginalRawMass apply add_nonneg · split_ifs <;> positivity · apply Finset.sum_nonneg intro i _ split_ifs · exact hw i · exact le_rfl

lemma commonMarginalRawMass_mul_outcome_sum {k d : Nat} (hd : 1 ≤ d) (hkd : k + 1 ≤ d) (reservoirMass : Real) (sign : Real → Real) (branch : Bool) (w : Fin k → Real) : ∑ x, commonMarginalRawMass hd hkd reservoirMass w x * commonMarginalOutcomeMean hd hkd sign branch w x = ∑ i, w i * (1 + (if branch then sign (w i) else -sign (w i))) / 2 := by simp_rw [commonMarginalOutcomeMean, Finset.mul_sum] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro i _ by_cases hi : w i = 0 · simp [hi] · rw [Finset.sum_eq_single (commonMarginalRareCell hkd i)] · rw [if_pos ⟨rfl, hi⟩, commonMarginalRawMass_rare] ring · intro x _ hxi simp [hxi] · simp

lemma finiteControlZeroAtom_nonneg {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (z : Obs d) : 0 ≤ finiteControlZeroAtom p e mu z := by unfold finiteControlZeroAtom split_ifs <;> try positivity · exact mul_nonneg (mul_nonneg (hp _).1 (he _).1) (hmu _).1 · exact mul_nonneg (mul_nonneg (hp _).1 (he _).1) (sub_nonneg.mpr (hmu _).2) · exact mul_nonneg (hp _).1 (sub_nonneg.mpr (he _).2)

lemma finiteControlZeroAtom_sum {d : Nat} (p e mu : Fin d → Real) (hp : ∑ x, p x = 1) : ∑ z : Obs d, finiteControlZeroAtom p e mu z = 1 := by simp only [Fintype.sum_prod_type, Fintype.sum_bool, finiteControlZeroAtom, Bool.false_eq_true, if_false, if_true] calc ∑ x, (p x * e x * mu x + p x * e x * (1 - mu x) + (0 + p x * (1 - e x))) = ∑ x, p x := by apply Finset.sum_congr rfl intro x _ ring _ = 1 := hp

lemma finiteControlZeroLaw_jointMass {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) (arm y : Bool) : jointMass (finiteControlZeroLaw p e mu hp he hmu hsum) x arm y = finiteControlZeroAtom p e mu (x, arm, y) := by unfold jointMass finiteControlZeroLaw rw [PMF.ofFintype_apply, ENNReal.toReal_ofReal] exact finiteControlZeroAtom_nonneg p e mu hp he hmu (x, arm, y)

lemma finiteControlZeroLaw_cellMass {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) : cellMass (finiteControlZeroLaw p e mu hp he hmu hsum) x = p x := by unfold cellMass simp only [Fintype.sum_bool, finiteControlZeroLaw_jointMass p e mu hp he hmu hsum, finiteControlZeroAtom, Bool.false_eq_true, if_false, if_true] ring

lemma finiteControlZeroLaw_armMass {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) : armMass (finiteControlZeroLaw p e mu hp he hmu hsum) x true = p x * e x := by unfold armMass simp only [Fintype.sum_bool, finiteControlZeroLaw_jointMass p e mu hp he hmu hsum, finiteControlZeroAtom, Bool.false_eq_true, if_false, if_true] ring

lemma finiteControlZeroLaw_armMass_false {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) : armMass (finiteControlZeroLaw p e mu hp he hmu hsum) x false = p x * (1 - e x) := by unfold armMass simp only [Fintype.sum_bool, finiteControlZeroLaw_jointMass p e mu hp he hmu hsum, finiteControlZeroAtom, Bool.false_eq_true, if_false, if_true] ring

lemma finiteControlZeroLaw_propensity {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) (hx : 0 < p x) : propensity (finiteControlZeroLaw p e mu hp he hmu hsum) x = e x := by rw [propensity, finiteControlZeroLaw_cellMass p e mu hp he hmu hsum, finiteControlZeroLaw_armMass p e mu hp he hmu hsum] field_simp [ne_of_gt hx]

lemma finiteControlZeroLaw_outcomeMean_true {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) (hx : 0 < p x * e x) : outcomeMean (finiteControlZeroLaw p e mu hp he hmu hsum) true x = mu x := by rw [outcomeMean, finiteControlZeroLaw_armMass p e mu hp he hmu hsum, finiteControlZeroLaw_jointMass] simp only [finiteControlZeroAtom, if_true] exact mul_div_cancel_left₀ (mu x) (ne_of_gt hx)

lemma finiteControlZeroLaw_outcomeMean_false {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (x : Fin d) : outcomeMean (finiteControlZeroLaw p e mu hp he hmu hsum) false x = 0 := by rw [outcomeMean, finiteControlZeroLaw_jointMass] simp [finiteControlZeroAtom]

lemma finiteControlZeroLaw_auxTable {d : Nat} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) : auxTableOf (finiteControlZeroLaw p e mu hp he hmu hsum) = fun z => if z.2 then p z.1 * e z.1 else p z.1 * (1 - e z.1) := by funext z cases z with | mk x arm => cases arm · unfold auxTableOf armMass simp [finiteControlZeroLaw_jointMass, finiteControlZeroAtom] · simp [auxTableOf, finiteControlZeroLaw_armMass]

lemma finiteControlZeroLaw_model {d : Nat} {eps : Real} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (hd : 2 ≤ d) (heps : 0 < eps) (hepsHalf : eps < 1 / 2) (hoverlap : ∀ x, 0 < p x → eps ≤ e x ∧ e x ≤ 1 - eps) : ModelClass d eps (finiteControlZeroLaw p e mu hp he hmu hsum) := by refine ⟨hd, heps, hepsHalf, ?_⟩ intro x hx rw [finiteControlZeroLaw_cellMass p e mu hp he hmu hsum] at hx rw [finiteControlZeroLaw_propensity p e mu hp he hmu hsum x hx] exact hoverlap x hx

lemma finiteControlZeroLaw_ate {d : Nat} {eps : Real} (p e mu : Fin d → Real) (hp : ∀ x, p x ∈ Icc (0 : Real) 1) (he : ∀ x, e x ∈ Icc (0 : Real) 1) (hmu : ∀ x, mu x ∈ Icc (0 : Real) 1) (hsum : ∑ x, p x = 1) (heps : 0 < eps) (hoverlap : ∀ x, 0 < p x → eps ≤ e x) : ateFunctional (finiteControlZeroLaw p e mu hp he hmu hsum) = ∑ x, p x * mu x := by unfold ateFunctional apply Finset.sum_congr rfl intro x _ rw [finiteControlZeroLaw_cellMass p e mu hp he hmu hsum, finiteControlZeroLaw_outcomeMean_false p e mu hp he hmu hsum] by_cases hx : p x = 0 · simp [hx] · have hpx : 0 < p x := lt_of_le_of_ne (hp x).1 (Ne.symm hx) have hex : 0 < e x := heps.trans_le (hoverlap x hpx) rw [finiteControlZeroLaw_outcomeMean_true p e mu hp he hmu hsum x (mul_pos hpx hex)] ring