Formalization: Minimax Mean Squared Error for Low-order Network Interference under Bernoulli Assignment

lemma E_coordinate_prod (d : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (g : Fin d → Bool → ℝ) : (blockDesign d p hp0 hp1).E (fun z => ∏ i, g i (z i)) = ∏ i, (p * g i true + (1 - p) * g i false) := by unfold blockDesign bernoulliDesign rw [FiniteDesign.E_prod_prod] apply Finset.prod_congr rfl intro i _ rw [coinDesign_E]

lemma E_centeredMonomial_mul (d : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (S T : Finset (Fin d)) : (blockDesign d p hp0 hp1).E (fun z => centeredMonomial p S z * centeredMonomial p T z) = if S = T then (p * (1 - p)) ^ S.card else 0 := by let x : Bool → ℝ := fun b => (if b then 1 else 0) - p have hpoint (z : Fin d → Bool) : centeredMonomial p S z * centeredMonomial p T z = ∏ i, (if i ∈ S then x (z i) else 1) * (if i ∈ T then x (z i) else 1) := by simp only [centeredMonomial, blockInd, x] rw [Finset.prod_mul_distrib] congr 1 <;> simp rw [show (fun z => centeredMonomial p S z * centeredMonomial p T z) = (fun z => ∏ i, ((if i ∈ S then x (z i) else 1) * (if i ∈ T then x (z i) else 1))) by funext z rw [hpoint z, Finset.prod_mul_distrib]] rw [E_coordinate_prod d p hp0 hp1 (fun i b => (if i ∈ S then x b else 1) * (if i ∈ T then x b else 1))] by_cases hST : S = T · subst T rw [if_pos rfl] have hfactor (i : Fin d) : p * ((if i ∈ S then x true else 1) * (if i ∈ S then x true else 1)) + (1 - p) * ((if i ∈ S then x false else 1) * (if i ∈ S then x false else 1)) = if i ∈ S then p * (1 - p) else 1 := by by_cases hi : i ∈ S <;> simp [hi, x] <;> ring simp_rw [hfactor] rw [Finset.prod_ite_mem] simp · rw [if_neg hST] have hdiff : ∃ i, (i ∈ S ∧ i ∉ T) ∨ (i ∈ T ∧ i ∉ S) := by by_contra h apply hST ext i constructor · intro hiS by_contra hiT exact h ⟨i, inl ⟨hiS, hiT⟩⟩ · intro hiT by_contra hiS exact h ⟨i, inr ⟨hiT, hiS⟩⟩ obtain ⟨i, hi⟩ := hdiff apply Finset.prod_eq_zero (Finset.mem_univ i) rcases hi with hi | hi · simp [hi.1, hi.2, x] <;> ring · simp [hi.1, hi.2, x] <;> ring

lemma E_centeredMonomial_mul_raw (d : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (S T : Finset (Fin d)) (hS : S.Nonempty) : (blockDesign d p hp0 hp1).E (fun z => centeredMonomial p S z * rawMonomial T z) = if S ⊆ T then (p * (1 - p)) ^ S.card * p ^ (T.card - S.card) else 0 := by let x : Bool → ℝ := fun b => (if b then 1 else 0) - p let y : Bool → ℝ := fun b => if b then 1 else 0 rw [show (fun z => centeredMonomial p S z * rawMonomial T z) = (fun z => ∏ i, ((if i ∈ S then x (z i) else 1) * (if i ∈ T then y (z i) else 1))) by funext z simp only [centeredMonomial, rawMonomial, blockInd, x, y] rw [Finset.prod_mul_distrib] congr 1 <;> simp] rw [E_coordinate_prod d p hp0 hp1 (fun i b => (if i ∈ S then x b else 1) * (if i ∈ T then y b else 1))] have hfactor (i : Fin d) : p * ((if i ∈ S then x true else 1) * (if i ∈ T then y true else 1)) + (1 - p) * ((if i ∈ S then x false else 1) * (if i ∈ T then y false else 1)) = if i ∈ S then (if i ∈ T then p * (1 - p) else 0) else if i ∈ T then p else 1 := by by_cases hiS : i ∈ S <;> by_cases hiT : i ∈ T <;> simp [hiS, hiT, x, y] <;> ring simp_rw [hfactor] by_cases hsub : S ⊆ T · rw [if_pos hsub] have hsimp (i : Fin d) : (if i ∈ S then (if i ∈ T then p * (1 - p) else 0) else if i ∈ T then p else 1) = if i ∈ S then p * (1 - p) else if i ∈ T then p else 1 := by by_cases hi : i ∈ S · simp [hi, hsub hi] · simp [hi] simp_rw [hsimp] have hsplit (i : Fin d) : (if i ∈ S then p * (1 - p) else if i ∈ T then p else 1) = (if i ∈ S then p * (1 - p) else 1) * (if i ∈ T \ S then p else 1) := by by_cases hiS : i ∈ S <;> by_cases hiT : i ∈ T <;> simp [hiS, hiT] simp_rw [hsplit, Finset.prod_mul_distrib] have hcard : (T \ S).card = T.card - S.card := by rw [Finset.card_sdiff, Finset.inter_eq_left.mpr hsub] rw [Finset.prod_ite_mem_eq, Finset.prod_ite_mem_eq] simp [hcard] · rw [if_neg hsub] obtain ⟨i, hiS, hiT⟩ : ∃ i, i ∈ S ∧ i ∉ T := by simpa only [Finset.not_subset] using hsub apply Finset.prod_eq_zero (Finset.mem_univ i) simp [hiS, hiT]

lemma FiniteDesign.E_prod_equiv {ι κ W : Type*} [Fintype ι] [Fintype κ] [Fintype W] [DecidableEq ι] [DecidableEq κ] (e : κ ≃ ι) (D : FiniteDesign W) (g : (κ → W) → ℝ) : (prodDesign (fun _ : ι => D)).E (fun z => g (fun k => z (e k))) = (prodDesign (fun _ : κ => D)).E g := by classical let q : (κ → W) ≃ (ι → W) := Equiv.arrowCongr e (Equiv.refl W) simp only [FiniteDesign.E, prodDesign_p] rw [← Equiv.sum_comp q] apply Finset.sum_congr rfl intro w hw have hq (i : ι) : q w i = w (e.symm i) := by simp [q, Equiv.arrowCongr] have harg : (fun k => q w (e k)) = w := by funext k rw [hq, e.symm_apply_apply] have hprod : (∏ i : ι, D.p (q w i)) = ∏ k : κ, D.p (w k) := by rw [← Equiv.prod_comp e (fun i : ι => D.p (q w i))] apply Finset.prod_congr rfl intro k hk rw [hq, e.symm_apply_apply] rw [harg, hprod]

lemma E_blockAssignment (n d : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (b : Fin (blockCount n d)) (g : (Fin d → Bool) → ℝ) : (bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1)).E (fun z => g (blockAssignment n d b z)) = (blockDesign d p hp0 hp1).E g := by classical let emb : Fin d → Fin n := fun k => ⟨b.val * d + k.val, by have hb : b.val < n / d := by simpa [blockCount] using b.isLt calc b.val * d + k.val < b.val * d + d := Nat.add_lt_add_left k.isLt _ _ = (b.val + 1) * d := by simp [Nat.add_mul] _ ≤ (n / d) * d := Nat.mul_le_mul_right d hb _ ≤ n := Nat.div_mul_le_self n d⟩ have hemb : Injective emb := by intro k l hkl apply Fin.ext have := congrArg val hkl dsimp [emb] at this omega let S : Finset (Fin n) := Finset.univ.image emb let e : Fin d ≃ ↥S := Equiv.ofBijective (fun k => (⟨emb k, Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩⟩ : ↥S)) ⟨by intro k l h exact hemb (congrArg val h), by intro j obtain ⟨k, hk, hkj⟩ := Finset.mem_image.mp j.property refine ⟨k, ?_⟩ apply Subtype.ext exact hkj⟩ let Dc : FiniteDesign Bool := coinDesign p hp0 hp1 let Dn : FiniteDesign (Fin n → Bool) := bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1) have hrestrict (z : Fin n → Bool) : blockAssignment n d b z = fun k => (S.restrict z) (e k) := by funext k rfl rw [show (bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1)).E (fun z => g (blockAssignment n d b z)) = ∫ z, g (blockAssignment n d b z) ∂Dn.toMeasure by exact (Dn.integral_toMeasure _).symm] rw [show Dn.toMeasure = Measure.pi (fun _ : Fin n => Dc.toMeasure) by exact prodDesign_toMeasure_eq_pi (fun _ : Fin n => Dc)] rw [← Measure.infinitePi_eq_pi] rw [show (fun z : Fin n → Bool => g (blockAssignment n d b z)) = (fun z => (fun w : ↥S → Bool => g (fun k => w (e k))) (S.restrict z)) by funext z rw [hrestrict]] have hr := MeasureTheory.integral_restrict_infinitePi (fun _ : Fin n => Dc.toMeasure) (s := S) (f := fun w : ↥S → Bool => g (fun k => w (e k))) (measurable_of_finite _).aestronglyMeasurable rw [hr] · rw [← prodDesign_toMeasure_eq_pi (fun _ : ↥S => Dc)] rw [FiniteDesign.integral_toMeasure] exact FiniteDesign.E_prod_equiv e Dc g

lemma blockPriorDensity_nonneg (n d β : ℕ) (B p σ : ℝ) (hB : 0 < B) (hp0 : 0 < p) (hp1 : p < 1) : 0 ≤ blockPriorDensity n d β B p σ := by intro x unfold blockPriorDensity assignmentMass apply mul_nonneg · apply Finset.prod_nonneg intro i hi split_ifs <;> linarith · apply Finset.prod_nonneg intro b hb exact cosSqDensity_nonneg (B / 2) (by linarith) _

lemma blockPriorDensity_integrable (n d β : ℕ) (B p σ : ℝ) (hB : 0 < B) (hp0 : 0 < p) (hp1 : p < 1) : Integrable (blockPriorDensity n d β B p σ) (blockDominatingMeasure n d) := by classical let shift : (Fin n → Bool) → Fin (blockCount n d) → ℝ := fun z b => σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z) have hinner (z : Fin n → Bool) : Integrable (fun y : Fin (blockCount n d) → ℝ => blockPriorDensity n d β B p σ (z, y)) (Measure.pi (fun _ : Fin (blockCount n d) => volume)) := by change Integrable (fun y => assignmentMass n p z * ∏ b, cosSqDensity (B / 2) (y b - shift z b)) (Measure.pi (fun _ : Fin (blockCount n d) => volume)) exact (Integrable.fintype_prod fun b => cosSqDensity_translate_integrable (B / 2) (shift z b)).const_mul _ have hmeas : AEStronglyMeasurable (blockPriorDensity n d β B p σ) (blockDominatingMeasure n d) := by apply Measurable.aestronglyMeasurable unfold blockPriorDensity apply mul · exact (measurable_of_finite (assignmentMass n p)).comp measurable_fst · apply Finset.measurable_prod intro b hb apply (cosSqDensity_measurable (B / 2)).comp apply Measurable.sub · exact (measurable_pi_apply b).comp measurable_snd · exact (measurable_of_finite (fun z : Fin n → Bool => shift z b)).comp measurable_fst rw [blockDominatingMeasure] at hmeas ⊢ rw [integrable_prod_iff hmeas] exact ⟨Filter.Eventually.of_forall hinner, Integrable.of_finite⟩

lemma hellingerSqDensity_pi_eq_two_mul_one_sub_affinity {ι : Type*} [Fintype ι] [DecidableEq ι] (f g : ι → ℝ → ℝ) (hf0 : ∀ i u, 0 ≤ f i u) (hg0 : ∀ i u, 0 ≤ g i u) (hfint : ∀ i, Integrable (f i) volume) (hgint : ∀ i, Integrable (g i) volume) (hf1 : ∀ i, ∫ u, f i u = 1) (hg1 : ∀ i, ∫ u, g i u = 1) (haint : ∀ i, Integrable (fun u => sqrt (f i u * g i u)) volume) : hellingerSqDensity (Measure.pi (fun _ : ι => volume)) (fun x => ∏ i, f i (x i)) (fun x => ∏ i, g i (x i)) = 2 * (1 - ∏ i, ∫ u, sqrt (f i u * g i u)) := by classical let F : (ι → ℝ) → ℝ := fun x => ∏ i, f i (x i) let G : (ι → ℝ) → ℝ := fun x => ∏ i, g i (x i) have hFint : Integrable F (Measure.pi (fun _ : ι => volume)) := Integrable.fintype_prod hfint have hGint : Integrable G (Measure.pi (fun _ : ι => volume)) := Integrable.fintype_prod hgint have hF0 : ∀ x, 0 ≤ F x := fun x => Finset.prod_nonneg fun i _ => hf0 i (x i) have hG0 : ∀ x, 0 ≤ G x := fun x => Finset.prod_nonneg fun i _ => hg0 i (x i) have hcross : Integrable (fun x => sqrt (F x * G x)) (Measure.pi (fun _ : ι => volume)) := by rw [show (fun x => sqrt (F x * G x)) = (fun x => ∏ i, sqrt (f i (x i) * g i (x i))) by funext x dsimp [F, G] rw [← Finset.prod_mul_distrib, Real.sqrt_prod] intro i hi exact mul_nonneg (hf0 i (x i)) (hg0 i (x i))] exact Integrable.fintype_prod haint unfold hellingerSqDensity have hpoint : (fun x => (sqrt (F x) - sqrt (G x)) ^ 2) = (fun x => F x + G x - 2 * sqrt (F x * G x)) := by funext x rw [Real.sqrt_mul (hF0 x)] nlinarith [Real.sq_sqrt (hF0 x), Real.sq_sqrt (hG0 x)] change ∫ x, (sqrt (F x) - sqrt (G x)) ^ 2 ∂(Measure.pi (fun _ : ι => volume)) = 2 * (1 - ∏ i, ∫ u, sqrt (f i u * g i u)) rw [hpoint] change ∫ x, (F + G) x - 2 * sqrt (F x * G x) ∂(Measure.pi (fun _ : ι => volume)) = 2 * (1 - ∏ i, ∫ u, sqrt (f i u * g i u)) rw [integral_sub (hFint.add hGint) (hcross.const_mul 2), show (∫ x, (F + G) x ∂Measure.pi (fun _ : ι => volume)) = ∫ x, F x + G x ∂Measure.pi (fun _ : ι => volume) by rfl, integral_add hFint hGint, integral_const_mul] rw [show (∫ x, F x ∂Measure.pi (fun _ : ι => volume)) = 1 by dsimp [F] rw [MeasureTheory.integral_fintype_prod_eq_prod] simp [hf1]] rw [show (∫ x, G x ∂Measure.pi (fun _ : ι => volume)) = 1 by dsimp [G] rw [MeasureTheory.integral_fintype_prod_eq_prod] simp [hg1]] rw [show (∫ x, sqrt (F x * G x) ∂Measure.pi (fun _ : ι => volume)) = ∏ i, ∫ u, sqrt (f i u * g i u) by exact densityAffinity_pi _ f g hf0 hg0] ring

lemma conditional_block_hellinger_le (n d β : ℕ) (B p : ℝ) (hB : 0 < B) (z : Fin n → Bool) : hellingerSqDensity (Measure.pi (fun _ : Fin (blockCount n d) => volume)) (fun y => ∏ b : Fin (blockCount n d), cosSqDensity (B / 2) (y b - tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z))) (fun y => ∏ b : Fin (blockCount n d), cosSqDensity (B / 2) (y b + tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z))) ≤ 4 * pi ^ 2 * tiltAmplitude B β p (blockCount n d) d ^ 2 / B ^ 2 * ∑ b : Fin (blockCount n d), blockRepresenter β p d (blockAssignment n d b z) ^ 2 := by classical let s : ℝ := B / 2 let δ : ℝ := tiltAmplitude B β p (blockCount n d) d let h : Fin (blockCount n d) → ℝ := fun b => blockRepresenter β p d (blockAssignment n d b z) let f : Fin (blockCount n d) → ℝ → ℝ := fun b u => cosSqDensity s (u - δ * h b) let g : Fin (blockCount n d) → ℝ → ℝ := fun b u => cosSqDensity s (u + δ * h b) have hs : 0 < s := by dsimp [s]; linarith have hf0 : ∀ b u, 0 ≤ f b u := fun b u => cosSqDensity_nonneg s hs _ have hg0 : ∀ b u, 0 ≤ g b u := fun b u => cosSqDensity_nonneg s hs _ have hfint : ∀ b, Integrable (f b) volume := fun b => cosSqDensity_translate_integrable s (δ * h b) have hgint : ∀ b, Integrable (g b) volume := by intro b simpa [g, sub_eq_add_neg, add_comm] using cosSqDensity_translate_integrable s (-δ * h b) have hf1 : ∀ b, ∫ u, f b u = 1 := fun b => cosSqDensity_translate_integral_one s (δ * h b) hs have hg1 : ∀ b, ∫ u, g b u = 1 := by intro b simpa [g, sub_eq_add_neg, add_comm] using cosSqDensity_translate_integral_one s (-δ * h b) hs have hflp (b : Fin (blockCount n d)) : MemLp (fun u => sqrt (f b u)) 2 volume := by have hasm : AEStronglyMeasurable (fun u => sqrt (f b u)) volume := (Real.continuous_sqrt.measurable.comp_aemeasurable (hfint b).aestronglyMeasurable.aemeasurable).aestronglyMeasurable rw [memLp_two_iff_integrable_sq hasm] rw [show (fun u => sqrt (f b u) ^ 2) = f b from funext fun u => Real.sq_sqrt (hf0 b u)] exact hfint b have hglp (b : Fin (blockCount n d)) : MemLp (fun u => sqrt (g b u)) 2 volume := by have hasm : AEStronglyMeasurable (fun u => sqrt (g b u)) volume := (Real.continuous_sqrt.measurable.comp_aemeasurable (hgint b).aestronglyMeasurable.aemeasurable).aestronglyMeasurable rw [memLp_two_iff_integrable_sq hasm] rw [show (fun u => sqrt (g b u) ^ 2) = g b from funext fun u => Real.sq_sqrt (hg0 b u)] exact hgint b have haint : ∀ b, Integrable (fun u => sqrt (f b u * g b u)) volume := by intro b have hEq : (fun u => sqrt (f b u * g b u)) = (fun u => sqrt (f b u)) * fun u => sqrt (g b u) := by funext u simp only [Pi.mul_apply] rw [Real.sqrt_mul (hf0 b u)] rw [hEq] exact (hflp b).integrable_mul (hglp b) change hellingerSqDensity (Measure.pi (fun _ : Fin (blockCount n d) => volume)) (fun y => ∏ b, f b (y b)) (fun y => ∏ b, g b (y b)) ≤ 4 * pi ^ 2 * δ ^ 2 / B ^ 2 * ∑ b, h b ^ 2 rw [hellingerSqDensity_pi_eq_two_mul_one_sub_affinity f g hf0 hg0 hfint hgint hf1 hg1 haint] calc 2 * (1 - ∏ b, ∫ u, sqrt (f b u * g b u)) ≤ 2 * ∑ b, (1 - ∫ u, sqrt (f b u * g b u)) := by gcongr apply one_sub_prod_le_sum · intro b exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun u => Real.sqrt_nonneg _) · intro b have hcs := MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg (p := (2 : ℝ)) (q := (2 : ℝ)) Real.HolderConjugate.two_two (Filter.Eventually.of_forall fun u => Real.sqrt_nonneg (f b u)) (Filter.Eventually.of_forall fun u => Real.sqrt_nonneg (g b u)) (by simpa using hflp b) (by simpa using hglp b) simp_rw [Real.rpow_two, Real.sq_sqrt (hf0 b _), Real.sq_sqrt (hg0 b _), hf1 b, hg1 b] at hcs simpa [Real.sqrt_mul (hf0 b _)] using hcs _ ≤ 2 * ∑ b, (pi ^ 2 * ((δ * h b) - (-δ * h b)) ^ 2 / (8 * s ^ 2)) := by gcongr with b simpa [f, g, sub_eq_add_neg] using cosSqDensity_affinity_defect_sharp s (δ * h b) (-δ * h b) hs _ = 4 * pi ^ 2 * δ ^ 2 / B ^ 2 * ∑ b, h b ^ 2 := by rw [Finset.mul_sum, Finset.mul_sum] apply Finset.sum_congr rfl intro b hb dsimp [s] field_simp ring

lemma E_sum_blockRepresenter_sq (n d β : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : (bernoulliDesign (fun _ : Fin n => p) (fun _ => le_of_lt hp0) (fun _ => le_of_lt hp1)).E (fun z => ∑ b : Fin (blockCount n d), blockRepresenter β p d (blockAssignment n d b z) ^ 2) = blockCount n d / blockEnergy β p d := by classical rw [FiniteDesign.E_sum] have hblock : (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun w => blockRepresenter β p d w ^ 2) = (blockEnergy β p d)⁻¹ := by let D := blockDesign d p (le_of_lt hp0) (le_of_lt hp1) have hD : IsProductBernoulli D p := by exact ⟨hp0, hp1, ⟨fun _ => le_of_lt hp0, fun _ => le_of_lt hp1, rfl⟩⟩ exact (blockRepresenter_contrast_energy β d p D hD hβ hd).2 rw [show (∑ b : Fin (blockCount n d), (bernoulliDesign (fun _ : Fin n => p) (fun _ => le_of_lt hp0) (fun _ => le_of_lt hp1)).E (fun z => blockRepresenter β p d (blockAssignment n d b z) ^ 2)) = ∑ _b : Fin (blockCount n d), (blockEnergy β p d)⁻¹ by apply Finset.sum_congr rfl intro b hb calc (bernoulliDesign (fun _ : Fin n => p) (fun _ => le_of_lt hp0) (fun _ => le_of_lt hp1)).E (fun z => blockRepresenter β p d (blockAssignment n d b z) ^ 2) = (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun w => blockRepresenter β p d w ^ 2) := E_blockAssignment n d p (le_of_lt hp0) (le_of_lt hp1) b (fun w => blockRepresenter β p d w ^ 2) _ = (blockEnergy β p d)⁻¹ := hblock] rw [Finset.sum_const] simp [nsmul_eq_mul, div_eq_mul_inv]

lemma sum_assignmentMass_mul_sum_blockRepresenter_sq (n d β : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : ∑ z : Fin n → Bool, assignmentMass n p z * (∑ b : Fin (blockCount n d), blockRepresenter β p d (blockAssignment n d b z) ^ 2) = blockCount n d / blockEnergy β p d := by let D := bernoulliDesign (fun _ : Fin n => p) (fun _ => le_of_lt hp0) (fun _ => le_of_lt hp1) have hprob (z : Fin n → Bool) : assignmentMass n p z = D.p z := by simp only [assignmentMass, D, bernoulliDesign, prodDesign_p, coinDesign] apply Finset.prod_congr rfl intro i hi cases z i <;> simp simp_rw [hprob] exact E_sum_blockRepresenter_sq n d β p hβ hd hp0 hp1

lemma blockPrior_hellinger_le (n d β : ℕ) (B p : ℝ) (hn : 1 ≤ n) (hd : 1 ≤ d) (hdn : d ≤ n) (hB : 0 < B) (hβ : 1 ≤ β) (hp0 : 0 < p) (hp1 : p < 1) : hellingerSqDensity (blockDominatingMeasure n d) (blockPriorDensity n d β B p 1) (blockPriorDensity n d β B p (-1)) ≤ 4 * pi ^ 2 * blockCount n d * tiltAmplitude B β p (blockCount n d) d ^ 2 / (B ^ 2 * blockEnergy β p d) := by classical let μy : Measure (Fin (blockCount n d) → ℝ) := Measure.pi (fun _ : Fin (blockCount n d) => volume) let δ := tiltAmplitude B β p (blockCount n d) d let Cplus : (Fin n → Bool) → (Fin (blockCount n d) → ℝ) → ℝ := fun z y => ∏ b, cosSqDensity (B / 2) (y b - δ * blockRepresenter β p d (blockAssignment n d b z)) let Cminus : (Fin n → Bool) → (Fin (blockCount n d) → ℝ) → ℝ := fun z y => ∏ b, cosSqDensity (B / 2) (y b + δ * blockRepresenter β p d (blockAssignment n d b z)) have hs : 0 < B / 2 := by linarith have ha0 (z : Fin n → Bool) : 0 ≤ assignmentMass n p z := by unfold assignmentMass apply Finset.prod_nonneg intro i hi split_ifs <;> linarith have hCplus0 (z) (y) : 0 ≤ Cplus z y := by dsimp [Cplus] exact Finset.prod_nonneg fun b _ => cosSqDensity_nonneg (B / 2) hs _ have hCminus0 (z) (y) : 0 ≤ Cminus z y := by dsimp [Cminus] exact Finset.prod_nonneg fun b _ => cosSqDensity_nonneg (B / 2) hs _ have hCplusInt (z) : Integrable (Cplus z) μy := by dsimp [Cplus, μy] exact Integrable.fintype_prod fun b => cosSqDensity_translate_integrable (B / 2) (δ * blockRepresenter β p d (blockAssignment n d b z)) have hCminusInt (z) : Integrable (Cminus z) μy := by dsimp [Cminus, μy] rw [show (fun y : Fin (blockCount n d) → ℝ => ∏ b, cosSqDensity (B / 2) (y b + δ * blockRepresenter β p d (blockAssignment n d b z))) = (fun y => ∏ b, cosSqDensity (B / 2) (y b - (-δ * blockRepresenter β p d (blockAssignment n d b z)))) by funext y apply Finset.prod_congr rfl intro b hb congr 2 ring] exact Integrable.fintype_prod fun b => cosSqDensity_translate_integrable (B / 2) (-δ * blockRepresenter β p d (blockAssignment n d b z)) have hhellInt (z) : Integrable (fun y => (sqrt (Cplus z y) - sqrt (Cminus z y)) ^ 2) μy := by have hmeas : AEStronglyMeasurable (fun y => (sqrt (Cplus z y) - sqrt (Cminus z y)) ^ 2) μy := by fun_prop apply Integrable.mono' ((hCplusInt z).const_mul 2 |>.add ((hCminusInt z).const_mul 2)) hmeas exact Filter.Eventually.of_forall fun y => by simp only [Pi.add_apply] rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [Real.sq_sqrt (hCplus0 z y), Real.sq_sqrt (hCminus0 z y), sq_nonneg (sqrt (Cplus z y) + sqrt (Cminus z y))] have hjointInt : Integrable (fun x : (Fin n → Bool) × (Fin (blockCount n d) → ℝ) => (sqrt (blockPriorDensity n d β B p 1 x) - sqrt (blockPriorDensity n d β B p (-1) x)) ^ 2) (blockDominatingMeasure n d) := by rw [blockDominatingMeasure] have hdensMeas (σ : ℝ) : Measurable (blockPriorDensity n d β B p σ) := by unfold blockPriorDensity apply mul · exact (measurable_of_finite (assignmentMass n p)).comp measurable_fst · apply Finset.measurable_prod intro b hb apply (cosSqDensity_measurable (B / 2)).comp apply Measurable.sub · exact (measurable_pi_apply b).comp measurable_snd · exact (measurable_of_finite (fun z : Fin n → Bool => σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z))).comp measurable_fst have hmeas : AEStronglyMeasurable (fun x : (Fin n → Bool) × (Fin (blockCount n d) → ℝ) => (sqrt (blockPriorDensity n d β B p 1 x) - sqrt (blockPriorDensity n d β B p (-1) x)) ^ 2) (Measure.count.prod μy) := by exact (((Real.continuous_sqrt.measurable.comp (hdensMeas 1)).sub (Real.continuous_sqrt.measurable.comp (hdensMeas (-1)))).pow_const 2).aestronglyMeasurable rw [integrable_prod_iff hmeas] constructor · exact Filter.Eventually.of_forall fun z => by have hz : (fun y => (sqrt (blockPriorDensity n d β B p 1 (z, y)) - sqrt (blockPriorDensity n d β B p (-1) (z, y))) ^ 2) = (fun y => assignmentMass n p z * (sqrt (Cplus z y) - sqrt (Cminus z y)) ^ 2) := by funext y simp only [blockPriorDensity, Cplus, Cminus, δ, one_mul, neg_one_mul, neg_mul, sub_neg_eq_add] change (sqrt (assignmentMass n p z * Cplus z y) - sqrt (assignmentMass n p z * Cminus z y)) ^ 2 = assignmentMass n p z * (sqrt (Cplus z y) - sqrt (Cminus z y)) ^ 2 rw [Real.sqrt_mul (ha0 z), Real.sqrt_mul (ha0 z), ← mul_sub, mul_pow] rw [Real.sq_sqrt (ha0 z)] rw [hz] exact (hhellInt z).const_mul (assignmentMass n p z) · exact Integrable.of_finite unfold hellingerSqDensity rw [blockDominatingMeasure, integral_prod _ hjointInt] have hinner (z : Fin n → Bool) : (∫ y, (sqrt (blockPriorDensity n d β B p 1 (z, y)) - sqrt (blockPriorDensity n d β B p (-1) (z, y))) ^ 2 ∂μy) = assignmentMass n p z * hellingerSqDensity μy (Cplus z) (Cminus z) := by rw [show (fun y => (sqrt (blockPriorDensity n d β B p 1 (z, y)) - sqrt (blockPriorDensity n d β B p (-1) (z, y))) ^ 2) = (fun y => assignmentMass n p z * (sqrt (Cplus z y) - sqrt (Cminus z y)) ^ 2) by funext y simp only [blockPriorDensity, Cplus, Cminus, δ, one_mul, neg_one_mul, neg_mul, sub_neg_eq_add] change (sqrt (assignmentMass n p z * Cplus z y) - sqrt (assignmentMass n p z * Cminus z y)) ^ 2 = assignmentMass n p z * (sqrt (Cplus z y) - sqrt (Cminus z y)) ^ 2 rw [Real.sqrt_mul (ha0 z), Real.sqrt_mul (ha0 z), ← mul_sub, mul_pow, Real.sq_sqrt (ha0 z)]] rw [integral_const_mul] rfl rw [show (fun z : Fin n → Bool => ∫ y, (sqrt (blockPriorDensity n d β B p 1 (z, y)) - sqrt (blockPriorDensity n d β B p (-1) (z, y))) ^ 2 ∂μy) = (fun z => assignmentMass n p z * hellingerSqDensity μy (Cplus z) (Cminus z)) by funext z exact hinner z] rw [MeasureTheory.integral_fintype] · have hcount (z : Fin n → Bool) : Measure.count.real ({z} : Set (Fin n → Bool)) = 1 := by rw [measureReal_def, Measure.count_apply_finite] · simp · exact Set.finite_singleton z simp_rw [hcount, one_smul] calc ∑ z : Fin n → Bool, assignmentMass n p z * hellingerSqDensity μy (Cplus z) (Cminus z) ≤ ∑ z : Fin n → Bool, assignmentMass n p z * (4 * pi ^ 2 * δ ^ 2 / B ^ 2 * ∑ b : Fin (blockCount n d), blockRepresenter β p d (blockAssignment n d b z) ^ 2) := by apply Finset.sum_le_sum intro z hz apply mul_le_mul_of_nonneg_left _ (ha0 z) exact conditional_block_hellinger_le n d β B p hB z _ = 4 * pi ^ 2 * δ ^ 2 / B ^ 2 * (blockCount n d / blockEnergy β p d) := by rw [show (∑ z : Fin n → Bool, assignmentMass n p z * (4 * pi ^ 2 * δ ^ 2 / B ^ 2 * ∑ b : Fin (blockCount n d), blockRepresenter β p d (blockAssignment n d b z) ^ 2)) = 4 * pi ^ 2 * δ ^ 2 / B ^ 2 * ∑ z : Fin n → Bool, assignmentMass n p z * (∑ b : Fin (blockCount n d), blockRepresenter β p d (blockAssignment n d b z) ^ 2) by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro z hz ring] rw [sum_assignmentMass_mul_sum_blockRepresenter_sq n d β p hβ hd hp0 hp1] _ = 4 * pi ^ 2 * blockCount n d * δ ^ 2 / (B ^ 2 * blockEnergy β p d) := by have hA : blockEnergy β p d ≠ 0 := ne_of_gt (blockEnergy_pos β d p hβ hd hp0 hp1) have hB0 : B ≠ 0 := ne_of_gt hB field_simp · exact Integrable.of_finite

lemma blockDesign_sq_eq_zero_iff (d : ℕ) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (f : (Fin d → Bool) → ℝ) : (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => f z ^ 2) = 0 ↔ f = 0 := by constructor · intro hf let D := blockDesign d p (le_of_lt hp0) (le_of_lt hp1) funext z have hnonneg (x : Fin d → Bool) : 0 ≤ D.p x * f x ^ 2 := mul_nonneg (D.p_nonneg x) (sq_nonneg (f x)) have hle : D.p z * f z ^ 2 ≤ ∑ x, D.p x * f x ^ 2 := Finset.single_le_sum (fun x _ => hnonneg x) (Finset.mem_univ z) have hterm : D.p z * f z ^ 2 = 0 := by apply le_antisymm · simpa [D, FiniteDesign.E] using hle.trans_eq hf · exact hnonneg z have hpz : 0 < D.p z := by dsimp [D] simp only [blockDesign, bernoulliDesign, prodDesign_p] apply Finset.prod_pos intro i hi simp only [coinDesign] cases h : z i <;> simp [h, hp0, hp1] exact sq_eq_zero_iff.mp (mul_eq_zero.mp hterm |>.resolve_left hpz.ne') · rintro rfl simp

lemma blockScore_mem_polySpace (β d : ℕ) (p : ℝ) : blockScore β p d ∈ polySpace β d := by rw [show blockScore β p d = fun z => ∑ r ∈ Icc 1 (effBeta β d), (bernoulliContrast p r / (p * (1 - p)) ^ r) * ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), ∏ j ∈ S, (blockInd z j - p) by rfl] rw [show (fun z => ∑ r ∈ Icc 1 (effBeta β d), (bernoulliContrast p r / (p * (1 - p)) ^ r) * ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), ∏ j ∈ S, (blockInd z j - p)) = ∑ r ∈ Icc 1 (effBeta β d), (bernoulliContrast p r / (p * (1 - p)) ^ r) • (fun z => ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), ∏ j ∈ S, (blockInd z j - p)) by funext z simp] apply Submodule.sum_mem intro r hr apply Submodule.smul_mem rw [show (fun z => ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), ∏ j ∈ S, (blockInd z j - p)) = ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), (fun z => ∏ j ∈ S, (blockInd z j - p)) by funext z simp] apply Submodule.sum_mem intro S hS have hScard : S.card = r := (Finset.mem_filter.mp hS).2 have hrle : r ≤ effBeta β d := (Finset.mem_Icc.mp hr).2 rw [show (fun z => ∏ j ∈ S, (blockInd z j - p)) = ∑ T ∈ S.powerset, (-p) ^ (S.card - T.card) • rawMonomial T by funext z simpa using centeredMonomial_raw_expansion d p S z] apply Submodule.sum_mem intro T hT apply Submodule.smul_mem rw [polySpace] apply Submodule.subset_span exact ⟨T, by refine ⟨?_, rfl⟩ exact (Finset.card_le_card (Finset.mem_powerset.mp hT)).trans (hScard.le.trans hrle)⟩

lemma weightFeasibleAt_represents (β d : ℕ) (D : FiniteDesign (Fin d → Bool)) (w : (Fin d → Bool) → ℝ) (hw : WeightFeasibleAt D β w) (f : (Fin d → Bool) → ℝ) (hf : f ∈ polySpace β d) : D.E (fun z => w z * f z) = contrastFunctional f := by rw [polySpace] at hf refine Submodule.span_induction (p := fun f _ => D.E (fun z => w z * f z) = contrastFunctional f) ?_ ?_ ?_ ?_ hf · intro f hf rcases hf with ⟨S, hScard, rfl⟩ by_cases hS : S.Nonempty · rw [hw.2 S hS hScard] unfold contrastFunctional rawMonomial have hz : (∏ j ∈ S, blockInd (fun _ => false) j) = 0 := by obtain ⟨j, hj⟩ := hS exact Finset.prod_eq_zero hj (by simp [blockInd]) rw [hz] simp [blockInd] · rw [Finset.not_nonempty_iff_eq_empty.mp hS] simpa [rawMonomial, contrastFunctional] using hw.1 · simp [contrastFunctional] · intro f g _ _ hf hg rw [show (fun z => w z * (f + g) z) = (fun z => w z * f z + w z * g z) by funext z simp [mul_add]] rw [D.E_add, hf, hg] simp [contrastFunctional] ring · intro a f _ hf rw [show (fun z => w z * (a • f) z) = (fun z => a * (w z * f z)) by funext z change w z * (a * f z) = a * (w z * f z) ring] rw [D.E_const_mul, hf] simp [contrastFunctional, mul_sub]

lemma perturbFeasible_energy_unique (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) (hβ : 1 ≤ β) (hd : 1 ≤ d) (h : (Fin d → Bool) → ℝ) (hh : PerturbFeasible β d h) : (blockEnergy β p d)⁻¹ ≤ D.E (fun z => h z ^ 2) ∧ (D.E (fun z => h z ^ 2) = (blockEnergy β p d)⁻¹ ↔ h = blockRepresenter β p d) := by let A := blockEnergy β p d let g := blockScore β p d have hA : 0 < A := blockEnergy_pos β d p hβ hd hD.1 hD.2.1 have hgh : D.E (fun z => g z * h z) = 1 := by simpa [g, hh.2] using blockScore_represents β d p D hD h hh.1 have hgg : D.E (fun z => g z ^ 2) = A := blockScore_sq_expectation β d p D hD have hsq : D.E (fun z => (A * h z - g z) ^ 2) = A ^ 2 * D.E (fun z => h z ^ 2) - A := by rw [show (fun z => (A * h z - g z) ^ 2) = (fun z => A ^ 2 * h z ^ 2 - 2 * A * (g z * h z) + g z ^ 2) by funext z ring] rw [D.E_add, D.E_sub, D.E_const_mul, D.E_const_mul, hgh, hgg] ring constructor · have hn := D.E_nonneg (fun z => sq_nonneg (A * h z - g z)) rw [hsq] at hn rw [inv_le_iff_one_le_mul₀ hA] nlinarith · constructor · intro heq change D.E (fun z => h z ^ 2) = A⁻¹ at heq have hz : D.E (fun z => (A * h z - g z) ^ 2) = 0 := by rw [hsq, heq] field_simp [hA.ne'] ring rcases hD with ⟨hp, hp', hpD⟩ have hDeq : D = blockDesign d p (le_of_lt hp) (le_of_lt hp') := by rcases hpD with ⟨hp0', hp1', rfl⟩ unfold blockDesign congr have hzero : (fun z => A * h z - g z) = 0 := by rw [hDeq] at hz exact (blockDesign_sq_eq_zero_iff d p hp hp' (fun z => A * h z - g z)).mp hz have hfun : h = fun z => g z / A := by funext z have hz := congrFun hzero z simp only [Pi.zero_apply] at hz apply (eq_div_iff hA.ne').2 linarith rw [hfun] funext z simp [blockRepresenter, Nat.ne_of_gt hd, g, A] · rintro rfl exact (blockRepresenter_contrast_energy β d p D hD hβ hd).2

lemma weightFeasibleAt_energy_unique (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) (w : (Fin d → Bool) → ℝ) (hw : WeightFeasibleAt D β w) : blockEnergy β p d ≤ D.E (fun z => w z ^ 2) ∧ (D.E (fun z => w z ^ 2) = blockEnergy β p d ↔ w = blockScore β p d) := by let A := blockEnergy β p d let g := blockScore β p d have hwg : D.E (fun z => w z * g z) = A := by rw [show A = contrastFunctional g by exact (blockScore_contrast β d p).symm] exact weightFeasibleAt_represents β d D w hw g (blockScore_mem_polySpace β d p) have hgg : D.E (fun z => g z ^ 2) = A := blockScore_sq_expectation β d p D hD have hsq : D.E (fun z => (w z - g z) ^ 2) = D.E (fun z => w z ^ 2) - A := by rw [show (fun z => (w z - g z) ^ 2) = (fun z => w z ^ 2 - 2 * (w z * g z) + g z ^ 2) by funext z ring] rw [D.E_add, D.E_sub, D.E_const_mul, hwg, hgg] ring constructor · have hn := D.E_nonneg (fun z => sq_nonneg (w z - g z)) rw [hsq] at hn linarith · constructor · intro heq have hz : D.E (fun z => (w z - g z) ^ 2) = 0 := by rw [hsq, heq] ring rcases hD with ⟨hp, hp', hpD⟩ have hDeq : D = blockDesign d p (le_of_lt hp) (le_of_lt hp') := by rcases hpD with ⟨hp0', hp1', rfl⟩ unfold blockDesign congr have hzero : (fun z => w z - g z) = 0 := by rw [hDeq] at hz exact (blockDesign_sq_eq_zero_iff d p hp hp' (fun z => w z - g z)).mp hz funext z have hz := congrFun hzero z simpa using sub_eq_zero.mp hz · rintro rfl exact hgg

lemma blockRepresenter_perturbFeasible (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) (hβ : 1 ≤ β) (hd : 1 ≤ d) : PerturbFeasible β d (blockRepresenter β p d) := by constructor · rw [show blockRepresenter β p d = (blockEnergy β p d)⁻¹ • blockScore β p d by funext z simp [blockRepresenter, Nat.ne_of_gt hd, div_eq_inv_mul]] exact Submodule.smul_mem _ _ (blockScore_mem_polySpace β d p) · exact (blockRepresenter_contrast_energy β d p D hD hβ hd).1

lemma blockPrograms_exact (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hp0' : 0 < p) (hp1' : p < 1) : perturbProg β d p hp0 hp1 = (blockEnergy β p d)⁻¹ ∧ weightProg β d p hp0 hp1 = blockEnergy β p d := by let D := blockDesign d p hp0 hp1 have hD : IsProductBernoulli D p := by exact ⟨hp0', hp1', ⟨fun _ => hp0, fun _ => hp1, rfl⟩⟩ have hrepFeas : PerturbFeasible β d (blockRepresenter β p d) := blockRepresenter_perturbFeasible β d p D hD hβ hd constructor · apply le_antisymm · apply csInf_le · refine ⟨0, ?_⟩ rintro q ⟨h, _hh, rfl⟩ exact D.E_nonneg (fun z => sq_nonneg (h z)) · refine ⟨blockRepresenter β p d, hrepFeas, ?_⟩ exact (blockRepresenter_contrast_energy β d p D hD hβ hd).2.symm · apply le_csInf · refine ⟨D.E (fun z => blockRepresenter β p d z ^ 2), ?_⟩ exact ⟨blockRepresenter β p d, hrepFeas, rfl⟩ intro q hq rcases hq with ⟨h, hh, rfl⟩ exact (perturbFeasible_energy_unique β d p D hD hβ hd h hh).1 · apply le_antisymm · apply csInf_le · refine ⟨0, ?_⟩ rintro q ⟨w, _hw, rfl⟩ exact D.E_nonneg (fun z => sq_nonneg (w z)) · refine ⟨blockScore β p d, ?_, ?_⟩ · exact blockScore_weightFeasibleAt β d p D hD · exact (blockScore_sq_expectation β d p D hD).symm · apply le_csInf · refine ⟨D.E (fun z => blockScore β p d z ^ 2), ?_⟩ exact ⟨blockScore β p d, blockScore_weightFeasibleAt β d p D hD, rfl⟩ intro q hq rcases hq with ⟨w, hw, rfl⟩ exact (weightFeasibleAt_energy_unique β d p D hD w hw).1

-- @node: lem:block-energy-representer lemma blockEnergy_representer : ∀ (β : ℕ) (p : ℝ), 1 ≤ β → 0 < p → p < 1 → ∃ c₁ c₂ H : ℝ, 0 < c₁ ∧ c₁ ≤ c₂ ∧ 0 < H ∧ ∀ (d : ℕ), 1 ≤ d → c₁ * (choose d (kStar d β p) : ℝ) ≤ blockEnergy β p d ∧ blockEnergy β p d ≤ c₂ * (choose d (kStar d β p) : ℝ) ∧ (∀ (D : FiniteDesign (Fin d → Bool)), IsProductBernoulli D p → (∀ f : (Fin d → Bool) → ℝ, f ∈ polySpace β d → D.E (fun z => blockScore β p d z * f z) = contrastFunctional f) ∧ contrastFunctional (blockRepresenter β p d) = 1 ∧ D.E (fun z => blockRepresenter β p d z ^ 2) = (blockEnergy β p d)⁻¹ ∧ PerturbFeasible β d (blockRepresenter β p d) ∧ (∀ h : (Fin d → Bool) → ℝ, PerturbFeasible β d h → (blockEnergy β p d)⁻¹ ≤ D.E (fun z => h z ^ 2) ∧ (D.E (fun z => h z ^ 2) = (blockEnergy β p d)⁻¹ ↔ h = blockRepresenter β p d)) ∧ (∀ w : (Fin d → Bool) → ℝ, WeightFeasibleAt D β w → blockEnergy β p d ≤ D.E (fun z => w z ^ 2) ∧ (D.E (fun z => w z ^ 2) = blockEnergy β p d ↔ w = blockScore β p d))) ∧ (∀ (hp0 : 0 ≤ p) (hp1 : p ≤ 1), perturbProg β d p hp0 hp1 = (blockEnergy β p d)⁻¹ ∧ weightProg β d p hp0 hp1 = blockEnergy β p d) ∧ (∑ T ∈ Finset.univ.powerset, |blockRawCoef β p d T|) ≤ H := by intro β p hβ hp0 hp1 let c₁ := blockLowerConst β p let c₂ := blockUpperConst β p let H := blockRawMassConst β p have hc₁ : 0 < c₁ := (blockLowerConst_spec β p hβ hp0 hp1).1 have hcomp1 := blockEnergy_uniform_compare β 1 p hβ (by omega) hp0 hp1 have hK : 0 < (choose 1 (kStar 1 β p) : ℝ) := by have hk := kStar_mem_exposedOrder β 1 p hβ (by omega) have hkle : kStar 1 β p ≤ 1 := (Finset.mem_Icc.mp (Finset.mem_filter.mp hk).1).2.trans (min_le_right β 1) exact_mod_cast Nat.choose_pos hkle have hc₁c₂ : c₁ ≤ c₂ := by dsimp [c₁, c₂] at hcomp1 ⊢ nlinarith have hH : 0 < H := by dsimp [H, blockRawMassConst, c₁] have hsum : 0 ≤ (((2 ^ β : ℕ) : ℝ) * ∑ r ∈ Icc 1 β, rawMassCoeff p r) / blockLowerConst β p := by apply div_nonneg · apply mul_nonneg (by positivity) apply sum_nonneg intro r hr simp only [rawMassCoeff] exact mul_nonneg (div_nonneg (abs_nonneg _) (pow_nonneg (mul_nonneg (le_of_lt hp0) (le_of_lt (sub_pos.mpr hp1))) r)) (pow_nonneg (by linarith) r) · exact le_of_lt ((blockLowerConst_spec β p hβ hp0 hp1).1) linarith refine ⟨c₁, c₂, H, hc₁, hc₁c₂, hH, ?_⟩ intro d hd have hcomp := blockEnergy_uniform_compare β d p hβ hd hp0 hp1 refine ⟨hcomp.1, hcomp.2, ?_, ?_, ?_⟩ · intro D hD refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ · intro f hf exact blockScore_represents β d p D hD f hf · exact (blockRepresenter_contrast_energy β d p D hD hβ hd).1 · exact (blockRepresenter_contrast_energy β d p D hD hβ hd).2 · exact blockRepresenter_perturbFeasible β d p D hD hβ hd · intro h hh exact perturbFeasible_energy_unique β d p D hD hβ hd h hh · intro w hw exact weightFeasibleAt_energy_unique β d p D hD w hw · intro hp0' hp1' exact blockPrograms_exact β d p hβ hd hp0' hp1' hp0 hp1 · exact blockRawCoef_mass_uniform β d p hβ hd hp0 hp1

lemma blockContrast_binomial (p : ℝ) (t : ℕ) (ht : 1 ≤ t) : ∑ r ∈ Icc 1 t, (Nat.choose t r : ℝ) * bernoulliContrast p r * p ^ (t - r) = 1 := by have hfull : (∑ r ∈ range (t + 1), (Nat.choose t r : ℝ) * bernoulliContrast p r * p ^ (t - r)) = 1 := by simp only [bernoulliContrast] rw [show (fun r => (Nat.choose t r : ℝ) * ((1 - p) ^ r - (-p) ^ r) * p ^ (t - r)) = (fun r => (Nat.choose t r : ℝ) * (1 - p) ^ r * p ^ (t - r) - (Nat.choose t r : ℝ) * (-p) ^ r * p ^ (t - r)) by funext r ring] rw [Finset.sum_sub_distrib] have h1 : (∑ r ∈ range (t + 1), (Nat.choose t r : ℝ) * (1 - p) ^ r * p ^ (t - r)) = 1 := by simpa [mul_comm, mul_left_comm, mul_assoc] using (add_pow (1 - p) p t).symm have h2 : (∑ r ∈ range (t + 1), (Nat.choose t r : ℝ) * (-p) ^ r * p ^ (t - r)) = 0 := by have ht0 : t ≠ 0 := by omega simpa [mul_comm, mul_left_comm, mul_assoc, ht0] using (add_pow (-p) p t).symm rw [h1, h2] norm_num rw [← hfull] apply Finset.sum_subset · intro r hr simp only [Finset.mem_Icc] at hr simp [hr.2] · intro r hrange hnot have hr0 : r = 0 := by simp only [Finset.mem_range] at hrange simp only [Finset.mem_Icc, not_and_or] at hnot omega subst r simp [bernoulliContrast]

lemma blockScore_raw_moment (β d : ℕ) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) (T : Finset (Fin d)) (hT : T.Nonempty) (hTcard : T.card ≤ effBeta β d) : (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => blockScore β p d z * rawMonomial T z) = 1 := by let v := p * (1 - p) have hv : v ≠ 0 := mul_ne_zero (ne_of_gt hp0) (ne_of_gt (sub_pos.mpr hp1)) have hmoment (S : Finset (Fin d)) (hS : S.Nonempty) : (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => (∏ j ∈ S, (blockInd z j - p)) * rawMonomial T z) = if S ⊆ T then v ^ S.card * p ^ (T.card - S.card) else 0 := by exact E_centeredMonomial_mul_raw d p (le_of_lt hp0) (le_of_lt hp1) S T hS simp only [blockScore, Finset.sum_mul, Finset.mul_sum, FiniteDesign.E_sum] simp_rw [mul_assoc, FiniteDesign.E_const_mul] rw [show (∑ r ∈ Icc 1 (effBeta β d), ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), bernoulliContrast p r / v ^ r * (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => (∏ j ∈ S, (blockInd z j - p)) * rawMonomial T z)) = ∑ r ∈ Icc 1 (effBeta β d), ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), bernoulliContrast p r / v ^ r * (if S ⊆ T then v ^ S.card * p ^ (T.card - S.card) else 0) by apply Finset.sum_congr rfl intro r hr apply Finset.sum_congr rfl intro S hS have hc : S.card = r := (Finset.mem_filter.mp hS).2 have hr1 : 1 ≤ r := (Finset.mem_Icc.mp hr).1 rw [hmoment S (Finset.card_pos.mp (by omega))]] rw [show (∑ r ∈ Icc 1 (effBeta β d), ∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), bernoulliContrast p r / v ^ r * (if S ⊆ T then v ^ S.card * p ^ (T.card - S.card) else 0)) = ∑ r ∈ Icc 1 (effBeta β d), (Nat.choose T.card r : ℝ) * bernoulliContrast p r * p ^ (T.card - r) by apply Finset.sum_congr rfl intro r hr rw [show Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r) = Finset.univ.powersetCard r by ext S simp [Finset.mem_powersetCard, eq_comm]] rw [show (∑ S ∈ Finset.univ.powersetCard r, bernoulliContrast p r / v ^ r * (if S ⊆ T then v ^ S.card * p ^ (T.card - S.card) else 0)) = ∑ S ∈ Finset.univ.powersetCard r, if S ⊆ T then bernoulliContrast p r * p ^ (T.card - r) else 0 by apply Finset.sum_congr rfl intro S hS have hScard : S.card = r := (Finset.mem_powersetCard.mp hS).2 rw [hScard] by_cases hs : S ⊆ T · simp only [if_pos hs] field_simp · simp [hs]] rw [← Finset.sum_filter] rw [show (Finset.univ.powersetCard r).filter (fun S => S ⊆ T) = T.powersetCard r by ext S simp [Finset.mem_powersetCard, and_comm]] rw [Finset.sum_const, Finset.card_powersetCard] simp [mul_assoc]] rw [show (∑ r ∈ Icc 1 (effBeta β d), (Nat.choose T.card r : ℝ) * bernoulliContrast p r * p ^ (T.card - r)) = ∑ r ∈ Icc 1 T.card, (Nat.choose T.card r : ℝ) * bernoulliContrast p r * p ^ (T.card - r) by symm apply Finset.sum_subset_zero_on_sdiff · intro r hr simp only [Finset.mem_Icc] at hr ⊢ exact ⟨hr.1, le_trans hr.2 hTcard⟩ · intro r hr have hlt : T.card < r := by simp only [mem_sdiff, Finset.mem_Icc, not_and_or] at hr omega simp [Nat.choose_eq_zero_of_lt hlt] · intro r hr rfl] exact blockContrast_binomial p T.card (Finset.card_pos.mpr hT)

lemma blockScore_mean_zero (β d : ℕ) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) : (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (blockScore β p d) = 0 := by have hmoment (S : Finset (Fin d)) (hS : S.Nonempty) : (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => ∏ j ∈ S, (blockInd z j - p)) = 0 := by have h := E_centeredMonomial_mul_raw d p (le_of_lt hp0) (le_of_lt hp1) S ∅ hS simpa [centeredMonomial, rawMonomial, hS.ne_empty] using h change (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => blockScore β p d z) = 0 simp only [blockScore] rw [FiniteDesign.E_sum] apply Finset.sum_eq_zero intro r hr rw [FiniteDesign.E_const_mul] rw [FiniteDesign.E_sum] rw [show (∑ S ∈ Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r), (blockDesign d p (le_of_lt hp0) (le_of_lt hp1)).E (fun z => ∏ j ∈ S, (blockInd z j - p))) = 0 by apply Finset.sum_eq_zero intro S hS have hScard : S.card = r := (Finset.mem_filter.mp hS).2 have hr1 : 1 ≤ r := (Finset.mem_Icc.mp hr).1 rw [hmoment S (Finset.card_pos.mp (by omega))]] ring

lemma blockScore_weightFeasibleAt (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) : WeightFeasibleAt D β (blockScore β p d) := by have hDeq : D = blockDesign d p (le_of_lt hD.1) (le_of_lt hD.2.1) := by rcases hD with ⟨hp, hp', hp0, hp1, rfl⟩ unfold blockDesign congr constructor · rw [hDeq] exact blockScore_mean_zero β d p hD.1 hD.2.1 · intro S hS hScard rw [hDeq] exact blockScore_raw_moment β d p hD.1 hD.2.1 S hS hScard

lemma blockScore_represents (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) (f : (Fin d → Bool) → ℝ) (hf : f ∈ polySpace β d) : D.E (fun z => blockScore β p d z * f z) = contrastFunctional f := by have hDeq : D = blockDesign d p (le_of_lt hD.1) (le_of_lt hD.2.1) := by rcases hD with ⟨hp, hp', hp0, hp1, rfl⟩ unfold blockDesign congr rw [hDeq] rw [polySpace] at hf refine Submodule.span_induction (p := fun f _ => (blockDesign d p (le_of_lt hD.1) (le_of_lt hD.2.1)).E (fun z => blockScore β p d z * f z) = contrastFunctional f) ?_ ?_ ?_ ?_ hf · intro f hf rcases hf with ⟨S, hScard, rfl⟩ by_cases hS : S.Nonempty · rw [blockScore_raw_moment β d p hD.1 hD.2.1 S hS hScard] have hfalse : (∏ j ∈ S, blockInd (fun _ : Fin d => false) j) = 0 := by obtain ⟨j, hj⟩ := hS apply Finset.prod_eq_zero hj simp [blockInd] unfold contrastFunctional rawMonomial rw [hfalse] simp [blockInd] · rw [Finset.not_nonempty_iff_eq_empty.mp hS] simpa [rawMonomial, contrastFunctional] using blockScore_mean_zero β d p hD.1 hD.2.1 · simp [contrastFunctional] · intro f g _ _ hf hg rw [show (fun z => blockScore β p d z * (f + g) z) = (fun z => blockScore β p d z * f z + blockScore β p d z * g z) by funext z simp [mul_add]] rw [FiniteDesign.E_add, hf, hg] simp [contrastFunctional] ring · intro a f _ hf rw [show (fun z => blockScore β p d z * (a • f) z) = (fun z => a * (blockScore β p d z * f z)) by funext z change blockScore β p d z * (a * f z) = a * (blockScore β p d z * f z) ring] rw [FiniteDesign.E_const_mul, hf] simp [contrastFunctional, mul_sub]

lemma blockScore_sq_expectation (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) : D.E (fun z => blockScore β p d z ^ 2) = blockEnergy β p d := by have hDeq : D = blockDesign d p (le_of_lt hD.1) (le_of_lt hD.2.1) := by rcases hD with ⟨hp, hp', hp0, hp1, rfl⟩ unfold blockDesign congr rw [hDeq] let hp0 : 0 ≤ p := le_of_lt hD.1 let hp1 : p ≤ 1 := le_of_lt hD.2.1 simp only [blockScore, pow_two, Finset.sum_mul, Finset.mul_sum, FiniteDesign.E_sum] have hmoment (r q : ℕ) (S T : Finset (Fin d)) : (blockDesign d p hp0 hp1).E (fun z => (bernoulliContrast p q / (p * (1 - p)) ^ q * ∏ j ∈ T, (blockInd z j - p)) * (bernoulliContrast p r / (p * (1 - p)) ^ r * ∏ j ∈ S, (blockInd z j - p))) = (bernoulliContrast p q / (p * (1 - p)) ^ q) * (bernoulliContrast p r / (p * (1 - p)) ^ r) * (if T = S then (p * (1 - p)) ^ T.card else 0) := by rw [show (fun z => (bernoulliContrast p q / (p * (1 - p)) ^ q * ∏ j ∈ T, (blockInd z j - p)) * (bernoulliContrast p r / (p * (1 - p)) ^ r * ∏ j ∈ S, (blockInd z j - p))) = (fun z => ((bernoulliContrast p q / (p * (1 - p)) ^ q) * (bernoulliContrast p r / (p * (1 - p)) ^ r)) * (centeredMonomial p T z * centeredMonomial p S z)) by funext z simp only [centeredMonomial] ring] rw [FiniteDesign.E_const_mul] rw [E_centeredMonomial_mul] simp_rw [hmoment] simp [blockEnergy] apply Finset.sum_congr rfl intro r hr have hr1 : 1 ≤ r := (Finset.mem_Icc.mp hr).1 have hrle : r ≤ effBeta β d := (Finset.mem_Icc.mp hr).2 rw [show (∑ S ∈ Finset.univ.powersetCard r, if S.Nonempty ∧ S.card ≤ effBeta β d then bernoulliContrast p S.card / (p * (1 - p)) ^ S.card * (bernoulliContrast p r / (p * (1 - p)) ^ r) * (p * (1 - p)) ^ S.card else 0) = ∑ _S ∈ Finset.univ.powersetCard r, bernoulliContrast p r / (p * (1 - p)) ^ r * (bernoulliContrast p r / (p * (1 - p)) ^ r) * (p * (1 - p)) ^ r by apply Finset.sum_congr rfl intro S hS have hScard : S.card = r := (Finset.mem_powersetCard.mp hS).2 have hSnonempty : S.Nonempty := by rw [Finset.nonempty_iff_ne_empty] intro h subst S simp at hScard omega simp [hScard, hSnonempty, hrle]] rw [Finset.sum_const, Finset.card_powersetCard] simp only [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] have hv : p * (1 - p) ≠ 0 := mul_ne_zero (ne_of_gt hD.1) (ne_of_gt (sub_pos.mpr hD.2.1)) field_simp

lemma weightProg_le_blockEnergy (β d : ℕ) (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) : weightProg β d p (le_of_lt hp0) (le_of_lt hp1) ≤ blockEnergy β p d := by let D := blockDesign d p (le_of_lt hp0) (le_of_lt hp1) have hD : IsProductBernoulli D p := by exact ⟨hp0, hp1, ⟨fun _ => le_of_lt hp0, fun _ => le_of_lt hp1, rfl⟩⟩ apply csInf_le · refine ⟨0, ?_⟩ rintro q ⟨w, _hw, rfl⟩ exact D.E_nonneg (fun z => sq_nonneg (w z)) · refine ⟨blockScore β p d, ?_, ?_⟩ · exact blockScore_weightFeasibleAt β d p D hD · exact (blockScore_sq_expectation β d p D hD).symm

lemma blockScore_contrast (β d : ℕ) (p : ℝ) : contrastFunctional (blockScore β p d) = blockEnergy β p d := by simp only [contrastFunctional, blockScore, blockInd, blockEnergy, Finset.sum_mul, Finset.sum_sub_distrib] have hsum_true (r : ℕ) : (∑ S ∈ (Finset.univ : Finset (Fin d)).powersetCard r, (1 - p) ^ S.card) = (Nat.choose d r : ℝ) * (1 - p) ^ r := by rw [show (∑ S ∈ (Finset.univ : Finset (Fin d)).powersetCard r, (1 - p) ^ S.card) = ∑ _S ∈ (Finset.univ : Finset (Fin d)).powersetCard r, (1 - p) ^ r by apply Finset.sum_congr rfl intro S hS rw [(Finset.mem_powersetCard.mp hS).2]] rw [Finset.sum_const, Finset.card_powersetCard] simp only [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] have hsum_false (r : ℕ) : (∑ S ∈ (Finset.univ : Finset (Fin d)).powersetCard r, (-p) ^ S.card) = (Nat.choose d r : ℝ) * (-p) ^ r := by rw [show (∑ S ∈ (Finset.univ : Finset (Fin d)).powersetCard r, (-p) ^ S.card) = ∑ _S ∈ (Finset.univ : Finset (Fin d)).powersetCard r, (-p) ^ r by apply Finset.sum_congr rfl intro S hS rw [(Finset.mem_powersetCard.mp hS).2]] rw [Finset.sum_const, Finset.card_powersetCard] simp only [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro r hr simp only [if_true, Bool.false_eq_true, if_false, Finset.prod_const] rw [show (Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r)) = (Finset.univ : Finset (Fin d)).powersetCard r by ext S simp [Finset.mem_powersetCard, eq_comm]] simp only [zero_sub] rw [hsum_true r, hsum_false r] simp only [bernoulliContrast] ring

lemma blockEnergy_pos (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : 0 < blockEnergy β p d := by have heff : 1 ≤ effBeta β d := by simp [effBeta, hβ, hd] have hmem : 1 ∈ Icc 1 (effBeta β d) := Finset.mem_Icc.mpr ⟨le_rfl, heff⟩ have hq : 0 < p * (1 - p) := mul_pos hp0 (sub_pos.mpr hp1) have hterm_nonneg (r : ℕ) : 0 ≤ (Nat.choose d r : ℝ) * bernoulliContrast p r ^ 2 / (p * (1 - p)) ^ r := by positivity have hterm_pos : 0 < (Nat.choose d 1 : ℝ) * bernoulliContrast p 1 ^ 2 / (p * (1 - p)) ^ 1 := by simp only [Nat.choose_one_right, bernoulliContrast, pow_one, neg_neg] have hdpos : 0 < (d : ℝ) := by exact_mod_cast hd rw [show (1 : ℝ) - p - -p = 1 by ring, one_pow, mul_one] exact div_pos hdpos hq unfold blockEnergy exact lt_of_lt_of_le hterm_pos (Finset.single_le_sum (fun r hr => hterm_nonneg r) hmem)

lemma blockRepresenter_contrast_energy (β d : ℕ) (p : ℝ) (D : FiniteDesign (Fin d → Bool)) (hD : IsProductBernoulli D p) (hβ : 1 ≤ β) (hd : 1 ≤ d) : contrastFunctional (blockRepresenter β p d) = 1 ∧ D.E (fun z => blockRepresenter β p d z ^ 2) = (blockEnergy β p d)⁻¹ := by have hApos := blockEnergy_pos β d p hβ hd hD.1 hD.2.1 have hdz : d ≠ 0 := Nat.ne_of_gt hd constructor · unfold contrastFunctional simp only [blockRepresenter, if_neg hdz] rw [← sub_div] rw [show blockScore β p d (fun _ => true) - blockScore β p d (fun _ => false) = blockEnergy β p d from blockScore_contrast β d p] exact div_self hApos.ne' · rw [show (fun z => blockRepresenter β p d z ^ 2) = (fun z => (blockEnergy β p d)⁻¹ ^ 2 * blockScore β p d z ^ 2) by funext z simp only [blockRepresenter, if_neg hdz] field_simp [hApos.ne']] rw [FiniteDesign.E_const_mul, blockScore_sq_expectation β d p D hD] field_simp [hApos.ne']

lemma centeredMonomial_raw_expansion (d : ℕ) (p : ℝ) (S : Finset (Fin d)) (z : Fin d → Bool) : ∏ j ∈ S, (blockInd z j - p) = ∑ T ∈ S.powerset, (-p) ^ (S.card - T.card) * rawMonomial T z := by rw [show (∏ j ∈ S, (blockInd z j - p)) = ∏ j ∈ S, (blockInd z j + (-p)) by simp [sub_eq_add_neg]] rw [Finset.prod_add] apply Finset.sum_congr rfl intro T hT have hsub : T ⊆ S := Finset.mem_powerset.mp hT rw [show (∏ i ∈ T, blockInd z i) = rawMonomial T z by rfl] rw [Finset.prod_const] rw [Finset.card_sdiff, Finset.inter_eq_left.mpr hsub] ring

lemma sum_powerset_subset_exchange {α : Type*} [Fintype α] [DecidableEq α] (A : Finset (Finset α)) (F : Finset α → Finset α → ℝ) : ∑ T ∈ (Finset.univ : Finset α).powerset, ∑ S ∈ A, (if T ⊆ S then F S T else 0) = ∑ S ∈ A, ∑ T ∈ S.powerset, F S T := by rw [Finset.sum_comm] apply Finset.sum_congr rfl intro S hS rw [← Finset.sum_filter] rw [show (Finset.univ : Finset α).powerset.filter (fun T => T ⊆ S) = S.powerset by ext T simp]

lemma blockRepresenter_raw_expansion (β d : ℕ) (p : ℝ) (hd : 1 ≤ d) (z : Fin d → Bool) : blockRepresenter β p d z = ∑ T ∈ Finset.univ.powerset, blockRawCoef β p d T * rawMonomial T z := by have hd0 : d ≠ 0 := Nat.ne_of_gt hd simp only [blockRepresenter, blockRawCoef, if_neg hd0, div_eq_inv_mul, blockScore] simp_rw [centeredMonomial_raw_expansion] let R := Icc 1 (effBeta β d) let A : ℕ → Finset (Finset (Fin d)) := fun r => Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r) let c : ℕ → ℝ := fun r => ((p * (1 - p)) ^ r)⁻¹ * bernoulliContrast p r let q : Finset (Fin d) → Finset (Fin d) → ℝ := fun S T => (-p) ^ (S.card - T.card) * rawMonomial T z change (blockEnergy β p d)⁻¹ * ∑ r ∈ R, c r * ∑ S ∈ A r, ∑ T ∈ S.powerset, q S T = ∑ T ∈ Finset.univ.powerset, ((blockEnergy β p d)⁻¹ * ∑ r ∈ R, ∑ S ∈ A r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0) * rawMonomial T z calc _ = (blockEnergy β p d)⁻¹ * ∑ r ∈ R, ∑ S ∈ A r, ∑ T ∈ S.powerset, c r * q S T := by congr 1 apply Finset.sum_congr rfl intro r hr rw [Finset.mul_sum] apply Finset.sum_congr rfl intro S hS rw [Finset.mul_sum] _ = (blockEnergy β p d)⁻¹ * ∑ r ∈ R, ∑ T ∈ Finset.univ.powerset, ∑ S ∈ A r, (if T ⊆ S then c r * q S T else 0) := by congr 1 apply Finset.sum_congr rfl intro r hr rw [sum_powerset_subset_exchange (A r) (fun S T => c r * q S T)] _ = (blockEnergy β p d)⁻¹ * ∑ T ∈ Finset.univ.powerset, ∑ r ∈ R, ∑ S ∈ A r, (if T ⊆ S then c r * q S T else 0) := by rw [Finset.sum_comm] _ = _ := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro T hT rw [show (∑ r ∈ R, ∑ S ∈ A r, if T ⊆ S then c r * q S T else 0) = (∑ r ∈ R, ∑ S ∈ A r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0) * rawMonomial T z by rw [Finset.sum_mul] apply Finset.sum_congr rfl intro r hr rw [Finset.sum_mul] apply Finset.sum_congr rfl intro S hS dsimp [q] by_cases hsub : T ⊆ S · simp only [if_pos hsub] ring · simp [hsub]] ring

lemma kStar_mem_exposedOrder (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) : kStar d β p ∈ (Icc 1 (effBeta β d)).filter (fun r => bernoulliContrast p r ≠ 0) := by let exposed := (Icc 1 (effBeta β d)).filter (fun r => bernoulliContrast p r ≠ 0) have heff : 1 ≤ effBeta β d := by simp [effBeta, hβ, hd] have hone : 1 ∈ exposed := by simp only [exposed, mem_filter, Finset.mem_Icc] exact ⟨⟨le_rfl, heff⟩, by norm_num [bernoulliContrast]⟩ have hne : exposed.Nonempty := ⟨1, hone⟩ rw [show kStar d β p = exposed.max' hne by simp only [kStar, exposed] rw [dif_pos hne]] exact Finset.max'_mem exposed hne

lemma blockEnergy_topExposed_le (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : (Nat.choose d (kStar d β p) : ℝ) * bernoulliContrast p (kStar d β p) ^ 2 / (p * (1 - p)) ^ kStar d β p ≤ blockEnergy β p d := by have hk := kStar_mem_exposedOrder β d p hβ hd have hkIcc : kStar d β p ∈ Icc 1 (effBeta β d) := (Finset.mem_filter.mp hk).1 have hv : 0 < p * (1 - p) := mul_pos hp0 (sub_pos.mpr hp1) unfold blockEnergy exact Finset.single_le_sum (fun r _ => show 0 ≤ (Nat.choose d r : ℝ) * bernoulliContrast p r ^ 2 / (p * (1 - p)) ^ r by positivity) hkIcc

lemma choose_le_pow_mul_choose (d r k β : ℕ) (hrk : r ≤ k) (hkd : k ≤ d) (hkβ : k ≤ β) : choose d r ≤ 2 ^ β * choose d k := by have hid := Nat.choose_mul (n := d) (k := k) (s := r) hrk have hone : 1 ≤ choose (d - r) (k - r) := Nat.choose_pos (by omega) have hfirst : choose d r ≤ choose d k * choose k r := by calc choose d r ≤ choose d r * choose (d - r) (k - r) := by nlinarith _ = choose d k * choose k r := hid.symm have hpow : choose k r ≤ 2 ^ β := by calc choose k r ≤ 2 ^ k := Nat.choose_le_two_pow k r _ ≤ 2 ^ β := Nat.pow_le_pow_right (by omega) hkβ nlinarith

lemma eligibleOrder_le_kStar (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (r : ℕ) (hr : r ∈ Icc 1 (effBeta β d)) (hrnz : bernoulliContrast p r ≠ 0) : r ≤ kStar d β p := by let exposed := (Icc 1 (effBeta β d)).filter (fun q => bernoulliContrast p q ≠ 0) have heff : 1 ≤ effBeta β d := by simp [effBeta, hβ, hd] have hone : 1 ∈ exposed := by simp only [exposed, mem_filter, Finset.mem_Icc] exact ⟨⟨le_rfl, heff⟩, by norm_num [bernoulliContrast]⟩ have hne : exposed.Nonempty := ⟨1, hone⟩ have hrmem : r ∈ exposed := Finset.mem_filter.mpr ⟨hr, hrnz⟩ rw [show kStar d β p = exposed.max' hne by simp only [kStar, exposed] rw [dif_pos hne]] exact Finset.le_max' exposed r hrmem

lemma blockLowerConst_spec (β : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hp0 : 0 < p) (hp1 : p < 1) : 0 < blockLowerConst β p ∧ ∀ r ∈ fixedExposed β p, blockLowerConst β p ≤ energyCoeff p r := by have hone : 1 ∈ fixedExposed β p := by simp only [fixedExposed, mem_filter, Finset.mem_Icc] exact ⟨⟨le_rfl, hβ⟩, by norm_num [bernoulliContrast]⟩ have hne : (fixedExposed β p).Nonempty := ⟨1, hone⟩ rw [blockLowerConst, dif_pos hne] constructor · have hm := Finset.min'_mem ((fixedExposed β p).image (energyCoeff p)) ((Finset.image_nonempty).mpr hne) rcases Finset.mem_image.mp hm with ⟨r, hr, heq⟩ rw [← heq] simp only [energyCoeff] have hrnz := (Finset.mem_filter.mp hr).2 exact div_pos (sq_pos_of_ne_zero hrnz) (pow_pos (mul_pos hp0 (sub_pos.mpr hp1)) r) · intro r hr apply Finset.min'_le exact Finset.mem_image.mpr ⟨r, hr, rfl⟩

lemma blockEnergy_uniform_compare (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : blockLowerConst β p * (Nat.choose d (kStar d β p) : ℝ) ≤ blockEnergy β p d ∧ blockEnergy β p d ≤ blockUpperConst β p * (Nat.choose d (kStar d β p) : ℝ) := by have hk := kStar_mem_exposedOrder β d p hβ hd have hkIcc := (Finset.mem_filter.mp hk).1 have hkd : kStar d β p ≤ d := (Finset.mem_Icc.mp hkIcc).2.trans (min_le_right β d) have hkβ : kStar d β p ≤ β := (Finset.mem_Icc.mp hkIcc).2.trans (min_le_left β d) have hkc : blockLowerConst β p ≤ energyCoeff p (kStar d β p) := by exact (blockLowerConst_spec β p hβ hp0 hp1).2 _ <| Finset.mem_filter.mpr ⟨ Finset.mem_Icc.mpr ⟨(Finset.mem_Icc.mp hkIcc).1, hkβ⟩, (Finset.mem_filter.mp hk).2⟩ constructor · calc blockLowerConst β p * (Nat.choose d (kStar d β p) : ℝ) ≤ (Nat.choose d (kStar d β p) : ℝ) * energyCoeff p (kStar d β p) := by rw [mul_comm] exact mul_le_mul_of_nonneg_left hkc (by positivity) _ ≤ blockEnergy β p d := by convert blockEnergy_topExposed_le β d p hβ hd hp0 hp1 using 1 <;> simp [energyCoeff] <;> ring · unfold blockUpperConst rw [show blockEnergy β p d = ∑ r ∈ Icc 1 (effBeta β d), (Nat.choose d r : ℝ) * energyCoeff p r by unfold blockEnergy apply Finset.sum_congr rfl intro r hr simp only [energyCoeff] ring] calc (∑ r ∈ Icc 1 (effBeta β d), (Nat.choose d r : ℝ) * energyCoeff p r) ≤ ∑ r ∈ Icc 1 (effBeta β d), (((2 ^ β : ℕ) : ℝ) * Nat.choose d (kStar d β p)) * energyCoeff p r := by apply Finset.sum_le_sum intro r hr by_cases hrnz : bernoulliContrast p r = 0 · simp [hrnz, energyCoeff] · have hc := choose_le_pow_mul_choose d r (kStar d β p) β (eligibleOrder_le_kStar β d p hβ hd r hr hrnz) hkd hkβ have hcoef : 0 ≤ energyCoeff p r := by simp only [energyCoeff] exact div_nonneg (sq_nonneg _) (pow_nonneg (mul_nonneg (le_of_lt hp0) (le_of_lt (sub_pos.mpr hp1))) r) gcongr exact_mod_cast hc _ ≤ ∑ r ∈ Icc 1 β, (((2 ^ β : ℕ) : ℝ) * Nat.choose d (kStar d β p)) * energyCoeff p r := by apply Finset.sum_le_sum_of_subset_of_nonneg · intro r hr simp only [Finset.mem_Icc] at hr ⊢ exact ⟨hr.1, hr.2.trans (min_le_left β d)⟩ · intro r _ _ simp only [energyCoeff] exact mul_nonneg (by positivity) <| div_nonneg (sq_nonneg _) (pow_nonneg (mul_nonneg (le_of_lt hp0) (le_of_lt (sub_pos.mpr hp1))) r) _ = (((2 ^ β : ℕ) : ℝ) * ∑ r ∈ Icc 1 β, energyCoeff p r) * Nat.choose d (kStar d β p) := by rw [← Finset.mul_sum] ring

lemma blockRawCoef_mass_estimate (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : (∑ T ∈ Finset.univ.powerset, |blockRawCoef β p d T|) ≤ (blockEnergy β p d)⁻¹ * ∑ r ∈ Icc 1 (effBeta β d), (Nat.choose d r : ℝ) * rawMassCoeff p r := by let A := blockEnergy β p d have hA : 0 < A := blockEnergy_pos β d p hβ hd hp0 hp1 have hd0 : d ≠ 0 := Nat.ne_of_gt hd let R := Icc 1 (effBeta β d) let F : ℕ → Finset (Finset (Fin d)) := fun r => Finset.univ.powerset.filter (fun S : Finset (Fin d) => S.card = r) let c : ℕ → ℝ := fun r => bernoulliContrast p r / (p * (1 - p)) ^ r simp only [blockRawCoef, if_neg hd0] rw [show (∑ T ∈ Finset.univ.powerset, |A⁻¹ * ∑ r ∈ R, ∑ S ∈ F r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0|) = A⁻¹ * ∑ T ∈ Finset.univ.powerset, |∑ r ∈ R, ∑ S ∈ F r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0| by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro T hT rw [abs_mul, abs_inv, abs_of_pos hA]] apply mul_le_mul_of_nonneg_left ?_ (le_of_lt (inv_pos.mpr hA)) calc (∑ T ∈ Finset.univ.powerset, |∑ r ∈ R, ∑ S ∈ F r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0|) ≤ ∑ T ∈ Finset.univ.powerset, ∑ r ∈ R, ∑ S ∈ F r, |if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0| := by apply Finset.sum_le_sum intro T hT calc |∑ r ∈ R, ∑ S ∈ F r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0| ≤ ∑ r ∈ R, |∑ S ∈ F r, if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0| := Finset.abs_sum_le_sum_abs _ _ _ ≤ _ := by apply Finset.sum_le_sum intro r hr exact Finset.abs_sum_le_sum_abs _ _ _ = ∑ r ∈ R, ∑ S ∈ F r, ∑ T ∈ S.powerset, |c r * (-p) ^ (S.card - T.card)| := by rw [Finset.sum_comm] apply Finset.sum_congr rfl intro r hr rw [show (∑ T ∈ Finset.univ.powerset, ∑ S ∈ F r, |if T ⊆ S then c r * (-p) ^ (S.card - T.card) else 0|) = ∑ T ∈ Finset.univ.powerset, ∑ S ∈ F r, if T ⊆ S then |c r * (-p) ^ (S.card - T.card)| else 0 by apply Finset.sum_congr rfl intro T hT apply Finset.sum_congr rfl intro S hS by_cases hsub : T ⊆ S <;> simp [hsub]] exact sum_powerset_subset_exchange (F r) (fun S T => |c r * (-p) ^ (S.card - T.card)|) _ = ∑ r ∈ R, (Nat.choose d r : ℝ) * rawMassCoeff p r := by apply Finset.sum_congr rfl intro r hr rw [show (∑ S ∈ F r, ∑ T ∈ S.powerset, |c r * (-p) ^ (S.card - T.card)|) = ∑ S ∈ F r, (|c r| * (1 + p) ^ r) by apply Finset.sum_congr rfl intro S hS have hScard : S.card = r := (Finset.mem_filter.mp hS).2 rw [show (∑ T ∈ S.powerset, |c r * (-p) ^ (S.card - T.card)|) = |c r| * ∑ T ∈ S.powerset, (1 : ℝ) ^ T.card * p ^ (S.card - T.card) by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro T hT rw [abs_mul, abs_pow, abs_neg, abs_of_pos hp0] simp] rw [Finset.sum_pow_mul_eq_add_pow, hScard]] rw [Finset.sum_const, show (F r).card = Nat.choose d r by simp [F, Finset.card_powersetCard]] simp only [nsmul_eq_mul, c, rawMassCoeff, abs_div, abs_pow, abs_of_pos (mul_pos hp0 (sub_pos.mpr hp1))]

lemma blockRawCoef_mass_uniform (β d : ℕ) (p : ℝ) (hβ : 1 ≤ β) (hd : 1 ≤ d) (hp0 : 0 < p) (hp1 : p < 1) : (∑ T ∈ Finset.univ.powerset, |blockRawCoef β p d T|) ≤ blockRawMassConst β p := by let c₁ := blockLowerConst β p let C := ((2 ^ β : ℕ) : ℝ) * ∑ r ∈ Icc 1 β, rawMassCoeff p r let K : ℝ := Nat.choose d (kStar d β p) let A := blockEnergy β p d have hc₁ : 0 < c₁ := (blockLowerConst_spec β p hβ hp0 hp1).1 have hA : 0 < A := blockEnergy_pos β d p hβ hd hp0 hp1 have hk := kStar_mem_exposedOrder β d p hβ hd have hkIcc := (Finset.mem_filter.mp hk).1 have hkd : kStar d β p ≤ d := (Finset.mem_Icc.mp hkIcc).2.trans (min_le_right β d) have hkβ : kStar d β p ≤ β := (Finset.mem_Icc.mp hkIcc).2.trans (min_le_left β d) have hK : 0 < K := by dsimp [K] exact_mod_cast Nat.choose_pos hkd have hC : 0 ≤ C := by dsimp [C] exact mul_nonneg (by positivity) <| sum_nonneg fun r hr => mul_nonneg (div_nonneg (abs_nonneg _) (pow_nonneg (mul_nonneg (le_of_lt hp0) (le_of_lt (sub_pos.mpr hp1))) r)) (pow_nonneg (by linarith) r) have hnum : (∑ r ∈ Icc 1 (effBeta β d), (Nat.choose d r : ℝ) * rawMassCoeff p r) ≤ C * K := by calc (∑ r ∈ Icc 1 (effBeta β d), (Nat.choose d r : ℝ) * rawMassCoeff p r) ≤ ∑ r ∈ Icc 1 (effBeta β d), (((2 ^ β : ℕ) : ℝ) * Nat.choose d (kStar d β p)) * rawMassCoeff p r := by apply Finset.sum_le_sum intro r hr by_cases hrnz : bernoulliContrast p r = 0 · simp [hrnz, rawMassCoeff] · have hc := choose_le_pow_mul_choose d r (kStar d β p) β (eligibleOrder_le_kStar β d p hβ hd r hr hrnz) hkd hkβ have hcoef : 0 ≤ rawMassCoeff p r := by simp only [rawMassCoeff] exact mul_nonneg (div_nonneg (abs_nonneg _) (pow_nonneg (mul_nonneg (le_of_lt hp0) (le_of_lt (sub_pos.mpr hp1))) r)) (pow_nonneg (by linarith) r) gcongr exact_mod_cast hc _ ≤ ∑ r ∈ Icc 1 β, (((2 ^ β : ℕ) : ℝ) * Nat.choose d (kStar d β p)) * rawMassCoeff p r := by apply Finset.sum_le_sum_of_subset_of_nonneg · intro r hr simp only [Finset.mem_Icc] at hr ⊢ exact ⟨hr.1, hr.2.trans (min_le_left β d)⟩ · intro r _ _ simp only [rawMassCoeff] exact mul_nonneg (by positivity) <| mul_nonneg (div_nonneg (abs_nonneg _) (pow_nonneg (mul_nonneg (le_of_lt hp0) (le_of_lt (sub_pos.mpr hp1))) r)) (pow_nonneg (by linarith) r) _ = C * K := by dsimp [C, K] rw [← Finset.mul_sum] ring have hlower : c₁ * K ≤ A := by exact (blockEnergy_uniform_compare β d p hβ hd hp0 hp1).1 calc (∑ T ∈ Finset.univ.powerset, |blockRawCoef β p d T|) ≤ A⁻¹ * ∑ r ∈ Icc 1 (effBeta β d), (Nat.choose d r : ℝ) * rawMassCoeff p r := blockRawCoef_mass_estimate β d p hβ hd hp0 hp1 _ ≤ A⁻¹ * (C * K) := by gcongr _ ≤ C / c₁ := by rw [show A⁻¹ * (C * K) = C * K / A by field_simp [hA.ne']] rw [div_le_iff₀ hA] calc C * K = (C / c₁) * (c₁ * K) := by field_simp [hc₁.ne'] _ ≤ (C / c₁) * A := mul_le_mul_of_nonneg_left hlower (div_nonneg hC (le_of_lt hc₁)) _ ≤ blockRawMassConst β p := by dsimp [blockRawMassConst, c₁, C] linarith

lemma zeroDegreeConventions_holds (β : ℕ) (p : ℝ) : ZeroDegreeConventions β p := by constructor · simp [effBeta] constructor · simp [kStar, effBeta] constructor · funext z simp [blockScore, effBeta] constructor · simp [blockEnergy, effBeta] constructor · funext z simp [blockRepresenter] · funext T simp [blockRawCoef]

lemma baselineProductDensity_nonneg (B : ℝ) (m : ℕ) (hB : 0 < B) : 0 ≤ baselineProductDensity B m := by intro U unfold baselineProductDensity apply Finset.prod_nonneg intro b hb unfold cosSqDensity split_ifs <;> positivity

lemma baselineProductDensity_integrable (B : ℝ) (m : ℕ) : Integrable (baselineProductDensity B m) (Measure.pi (fun _ : Fin m => volume)) := by unfold baselineProductDensity exact Integrable.fintype_prod fun _ => cosSqDensity_integrable (B / 2)

lemma baselineProductDensity_integral_one (B : ℝ) (m : ℕ) (hB : 0 < B) : ∫ U, baselineProductDensity B m U ∂(Measure.pi (fun _ : Fin m => volume)) = 1 := by unfold baselineProductDensity rw [MeasureTheory.integral_fintype_prod_eq_prod] simp_rw [cosSqDensity_integral_one (B / 2) (by linarith)] simp

lemma baselineProductMeasure_isProbability (B : ℝ) (m : ℕ) (hB : 0 < B) : IsProbabilityMeasure (baselineProductMeasure B m) := by rw [isProbabilityMeasure_iff_real] unfold baselineProductMeasure rw [measureReal_def, withDensity_apply _ MeasurableSet.univ] rw [setLIntegral_univ] rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal (baselineProductDensity_integrable B m)] · rw [baselineProductDensity_integral_one B m hB] simp · exact Filter.Eventually.of_forall (baselineProductDensity_nonneg B m hB)

lemma blockObservedVector_measurable (n d : ℕ) : Measurable (blockObservedVector n d) := by apply measurable_pi_lambda intro i by_cases hi : i.val < activeCount n d · simp only [blockObservedVector, dif_pos hi] fun_prop · simp [blockObservedVector, hi]

lemma blockEstimatorStatistic_measurable (n d : ℕ) (est : Estimator (Fin n)) (hest : OutcomeMeasurable est) : Measurable (blockEstimatorStatistic n d est) := by classical let G : Fin n → Fin n → Bool := fun j i => decide (blockGraph n d j i) have hsum : Measurable (fun x : (Fin n → Bool) × (Fin (blockCount n d) → ℝ) => ∑ z : Fin n → Bool, if x.1 = z then est G z (blockObservedVector n d x) else 0) := by apply measurable_sum univ intro z hz apply Measurable.ite · exact (measurableSet_singleton z).preimage measurable_fst · apply (hest G z).comp exact blockObservedVector_measurable n d · exact measurable_const convert hsum using 1 funext x simp [blockEstimatorStatistic, G]

lemma blockObservedVector_translate (n d β : ℕ) (B p σ : ℝ) (hd : 1 ≤ d) (hσ : σ = -1 ∨ σ = 1) (z : Fin n → Bool) (U : Fin (blockCount n d) → ℝ) : blockObservedVector n d (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) = obsOutcome (blockGraph n d) (blockSchedule n d β B p σ hσ U) z := by funext i by_cases hi : i.val < activeCount n d · rw [show blockObservedVector n d (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) i = U ⟨i.val / d, by simp only [activeCount] at hi rw [div_lt_iff_lt_mul (by omega)] simpa [mul_comm] using hi⟩ + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d ⟨i.val / d, by simp only [activeCount] at hi rw [div_lt_iff_lt_mul (by omega)] simpa [mul_comm] using hi⟩ z) by simp [blockObservedVector, hi]] exact (potentialOutcome_blockSchedule n d β B p σ hd hσ U i hi z).symm · rw [show blockObservedVector n d (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) i = 0 by simp [blockObservedVector, hi]] exact (potentialOutcome_blockSchedule_inactive n d β B p σ hσ U i hi z).symm

lemma blockPrior_integral_eq_baseline (n d β : ℕ) (B p σ : ℝ) (hB : 0 < B) (hp0 : 0 < p) (hp1 : p < 1) (φ : ((Fin n → Bool) × (Fin (blockCount n d) → ℝ)) → ℝ) (hφ : Measurable φ) (hφ0 : ∀ x, 0 ≤ φ x) (hφ1 : ∀ x, φ x ≤ 1) : ∫ x, blockPriorDensity n d β B p σ x * φ x ∂blockDominatingMeasure n d = ∫ U, baselineProductDensity B (blockCount n d) U * ∑ z : Fin n → Bool, assignmentMass n p z * φ (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) ∂(Measure.pi (fun _ : Fin (blockCount n d) => volume)) := by classical let μy : Measure (Fin (blockCount n d) → ℝ) := Measure.pi (fun _ : Fin (blockCount n d) => volume) let shift : (Fin n → Bool) → Fin (blockCount n d) → ℝ := fun z b => σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z) have hleftInt : Integrable (fun x => blockPriorDensity n d β B p σ x * φ x) (blockDominatingMeasure n d) := by apply Integrable.mono' (blockPriorDensity_integrable n d β B p σ hB hp0 hp1) ((blockPriorDensity_integrable n d β B p σ hB hp0 hp1).1.mul hφ.aestronglyMeasurable) exact Filter.Eventually.of_forall fun x => by change |blockPriorDensity n d β B p σ x * φ x| ≤ blockPriorDensity n d β B p σ x rw [abs_mul, abs_of_nonneg (blockPriorDensity_nonneg n d β B p σ hB hp0 hp1 x), abs_of_nonneg (hφ0 x)] exact mul_le_of_le_one_right (blockPriorDensity_nonneg n d β B p σ hB hp0 hp1 x) (hφ1 x) rw [blockDominatingMeasure, integral_prod _ hleftInt] have htranslate (z : Fin n → Bool) : (∫ y, blockPriorDensity n d β B p σ (z, y) * φ (z, y) ∂μy) = assignmentMass n p z * ∫ U, baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b) ∂μy := by change (∫ y, (assignmentMass n p z * ∏ b, cosSqDensity (B / 2) (y b - shift z b)) * φ (z, y) ∂μy) = assignmentMass n p z * ∫ U, baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b) ∂μy rw [show (∫ y, (assignmentMass n p z * ∏ b, cosSqDensity (B / 2) (y b - shift z b)) * φ (z, y) ∂μy) = assignmentMass n p z * ∫ y, (∏ b, cosSqDensity (B / 2) (y b - shift z b)) * φ (z, y) ∂μy by rw [← integral_const_mul] apply integral_congr_ae exact Filter.Eventually.of_forall fun y => by ring] congr 1 rw [← MeasureTheory.integral_add_right_eq_self (fun y => (∏ b, cosSqDensity (B / 2) (y b - shift z b)) * φ (z, y)) (shift z)] apply integral_congr_ae exact Filter.Eventually.of_forall fun U => by change (∏ b, cosSqDensity (B / 2) ((U + shift z) b - shift z b)) * φ (z, U + shift z) = baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b) congr 1 · unfold baselineProductDensity apply Finset.prod_congr rfl intro b hb congr 2 simp change (∫ x, ∫ y, blockPriorDensity n d β B p σ (x, y) * φ (x, y) ∂μy ∂Measure.count) = ∫ U, baselineProductDensity B (blockCount n d) U * ∑ z : Fin n → Bool, assignmentMass n p z * φ (z, fun b => U b + shift z b) ∂μy simp_rw [htranslate] rw [MeasureTheory.integral_fintype] · have hcount (z : Fin n → Bool) : Measure.count.real ({z} : Set (Fin n → Bool)) = 1 := by rw [measureReal_def, Measure.count_apply_finite] · simp · exact Set.finite_singleton z simp_rw [hcount, one_smul] rw [show (∑ z : Fin n → Bool, assignmentMass n p z * ∫ U, baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b) ∂μy) = ∫ U, ∑ z : Fin n → Bool, assignmentMass n p z * (baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b)) ∂μy by rw [integral_finset_sum] · apply Finset.sum_congr rfl intro z hz rw [integral_const_mul] · intro z hz have hcomp : AEStronglyMeasurable (fun U : Fin (blockCount n d) → ℝ => φ (z, fun b => U b + shift z b)) μy := (hφ.comp (measurable_const.prodMk (measurable_id.add measurable_const))).aestronglyMeasurable have hmul : Integrable (fun U : Fin (blockCount n d) → ℝ => baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b)) μy := (baselineProductDensity_integrable B (blockCount n d)).mono' ((baselineProductDensity_integrable B (blockCount n d)).1.mul hcomp) (Filter.Eventually.of_forall fun U => by change |baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b)| ≤ baselineProductDensity B (blockCount n d) U rw [abs_mul, abs_of_nonneg (baselineProductDensity_nonneg B (blockCount n d) hB U), abs_of_nonneg (hφ0 _)] exact mul_le_of_le_one_right (baselineProductDensity_nonneg B (blockCount n d) hB U) (hφ1 _)) exact hmul.const_mul (assignmentMass n p z)] apply integral_congr_ae exact Filter.Eventually.of_forall fun U => by change (∑ z : Fin n → Bool, assignmentMass n p z * (baselineProductDensity B (blockCount n d) U * φ (z, fun b => U b + shift z b))) = baselineProductDensity B (blockCount n d) U * ∑ z : Fin n → Bool, assignmentMass n p z * φ (z, fun b => U b + shift z b) rw [Finset.mul_sum] apply Finset.sum_congr rfl intro z hz ring · exact Integrable.of_finite

lemma blockPriorLaw_isProbability (n d β : ℕ) (B p σ : ℝ) (hn : 1 ≤ n) (hd : 1 ≤ d) (hdn : d ≤ n) (hB : 0 < B) (hp0 : 0 < p) (hp1 : p < 1) (hσ : σ = -1 ∨ σ = 1) : IsProbabilityMeasure (blockPriorLaw n d β B p σ) := by rw [isProbabilityMeasure_iff_real] unfold blockPriorLaw rw [measureReal_def, withDensity_apply _ MeasurableSet.univ, setLIntegral_univ] rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal (blockPriorDensity_integrable n d β B p σ hB hp0 hp1)] · rw [blockPriorDensity_integral_one n d β B p σ hn hd hdn hB hp0 hp1 hσ] simp · exact Filter.Eventually.of_forall (blockPriorDensity_nonneg n d β B p σ hB hp0 hp1)

lemma blockPrior_tvDist_le_sqrt_hellinger (n d β : ℕ) (B p : ℝ) (hn : 1 ≤ n) (hd : 1 ≤ d) (hdn : d ≤ n) (hB : 0 < B) (hp0 : 0 < p) (hp1 : p < 1) : tvDist (blockPriorLaw n d β B p 1) (blockPriorLaw n d β B p (-1)) ≤ sqrt (hellingerSqDensity (blockDominatingMeasure n d) (blockPriorDensity n d β B p 1) (blockPriorDensity n d β B p (-1))) := by let μ := blockDominatingMeasure n d let f := blockPriorDensity n d β B p 1 let g := blockPriorDensity n d β B p (-1) have hf := blockPriorDensity_integrable n d β B p 1 hB hp0 hp1 have hg := blockPriorDensity_integrable n d β B p (-1) hB hp0 hp1 have hf0 := blockPriorDensity_nonneg n d β B p 1 hB hp0 hp1 have hg0 := blockPriorDensity_nonneg n d β B p (-1) hB hp0 hp1 have hf1 := blockPriorDensity_integral_one n d β B p 1 hn hd hdn hB hp0 hp1 (inr rfl) have hg1 := blockPriorDensity_integral_one n d β B p (-1) hn hd hdn hB hp0 hp1 (inl rfl) have htv := tvDist_le_sqrt_two_mul_one_sub_affinity μ f g hf hg hf0 hg0 hf1 hg1 have hhell := hellingerSqDensity_eq_two_mul_one_sub_affinity μ f g hf hg hf0 hg0 hf1 hg1 simpa [blockPriorLaw, μ, f, g, hhell] using htv

lemma missIndicator_measurable {Ω : Type*} [MeasurableSpace Ω] (T : Ω → ℝ) (hT : Measurable T) (θ s : ℝ) : Measurable (missIndicator T θ s) := by unfold missIndicator apply Measurable.ite · exact measurableSet_le measurable_const ((continuous_abs.measurable).comp (hT.sub measurable_const)) · exact measurable_const · exact measurable_const

lemma missIndicator_nonneg {Ω : Type*} (T : Ω → ℝ) (θ s : ℝ) : 0 ≤ missIndicator T θ s := by intro x unfold missIndicator split <;> norm_num

lemma missIndicator_le_one {Ω : Type*} (T : Ω → ℝ) (θ s : ℝ) : missIndicator T θ s ≤ 1 := by intro x unfold missIndicator split <;> norm_num

lemma assignmentMass_eq_bernoulli_p (n : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (z : Fin n → Bool) : assignmentMass n p z = (bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1)).p z := by simp [assignmentMass, bernoulliDesign, prodDesign_p, coinDesign] apply Finset.prod_congr rfl intro i hi cases hzi : z i <;> simp [hzi]

lemma sum_assignmentMass_one (n : ℕ) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : ∑ z : Fin n → Bool, assignmentMass n p z = 1 := by simp_rw [assignmentMass_eq_bernoulli_p n p hp0 hp1] exact (bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1)).p_sum

lemma blockPriorLaw_real_miss (n d β : ℕ) (B p σ θ s : ℝ) (hB : 0 < B) (hp0 : 0 < p) (hp1 : p < 1) (est : Estimator (Fin n)) (hest : OutcomeMeasurable est) : (blockPriorLaw n d β B p σ).real {x | s ≤ |blockEstimatorStatistic n d est x - θ|} = ∫ U, baselineProductDensity B (blockCount n d) U * ∑ z : Fin n → Bool, assignmentMass n p z * missIndicator (blockEstimatorStatistic n d est) θ s (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) ∂(Measure.pi (fun _ : Fin (blockCount n d) => volume)) := by let T := blockEstimatorStatistic n d est have hT : Measurable T := blockEstimatorStatistic_measurable n d est hest have hmiss : Measurable (missIndicator T θ s) := missIndicator_measurable T hT θ s have hdens := blockPriorDensity_integrable n d β B p σ hB hp0 hp1 have hset : MeasurableSet {x | s ≤ |T x - θ|} := by exact measurableSet_le measurable_const ((continuous_abs.measurable).comp (hT.sub measurable_const)) have hreal : (blockPriorLaw n d β B p σ).real {x | s ≤ |T x - θ|} = ∫ x in {x | s ≤ |T x - θ|}, blockPriorDensity n d β B p σ x ∂blockDominatingMeasure n d := by rw [blockPriorLaw, measureReal_def, withDensity_apply _ hset] rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal hdens.integrableOn] · rw [ENNReal.toReal_ofReal] exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun x => blockPriorDensity_nonneg n d β B p σ hB hp0 hp1 x) · exact Filter.Eventually.of_forall (blockPriorDensity_nonneg n d β B p σ hB hp0 hp1) rw [hreal] rw [← integral_indicator hset] have hind : indicator {x | s ≤ |T x - θ|} (blockPriorDensity n d β B p σ) = fun x => blockPriorDensity n d β B p σ x * missIndicator T θ s x := by funext x by_cases hx : s ≤ |T x - θ| · simp [indicator, missIndicator, hx] · simp [indicator, missIndicator, hx] rw [hind] exact blockPrior_integral_eq_baseline n d β B p σ hB hp0 hp1 (missIndicator T θ s) hmiss (missIndicator_nonneg T θ s) (missIndicator_le_one T θ s)

lemma measurableSet_blockBaselineSupport (B : ℝ) (m : ℕ) : MeasurableSet {U : Fin m → ℝ | blockBaselineSupport B U} := by rw [show {U : Fin m → ℝ | blockBaselineSupport B U} = ⋂ b : Fin m, {U | |U b| ≤ B / 2} by ext U simp [blockBaselineSupport]] exact MeasurableSet.iInter fun b => measurableSet_le ((continuous_abs.measurable).comp (measurable_pi_apply b)) measurable_const

lemma baselineProductDensity_eq_zero_of_not_support (B : ℝ) (m : ℕ) (U : Fin m → ℝ) (hU : ¬ blockBaselineSupport B U) : baselineProductDensity B m U = 0 := by classical obtain ⟨b, hb⟩ := not_forall.mp hU unfold baselineProductDensity apply Finset.prod_eq_zero (Finset.mem_univ b) unfold cosSqDensity rw [if_neg hb]

lemma blockMissProbability_measurable (n d β : ℕ) (B p σ θ s : ℝ) (est : Estimator (Fin n)) (hest : OutcomeMeasurable est) : Measurable (blockMissProbability n d β B p σ θ s est) := by classical unfold blockMissProbability apply measurable_sum intro z hz apply const_mul exact (missIndicator_measurable _ (blockEstimatorStatistic_measurable n d est hest) θ s).comp (measurable_const.prodMk (measurable_id.add measurable_const))

lemma blockMissProbability_bounds (n d β : ℕ) (B p σ θ s : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (est : Estimator (Fin n)) (U : Fin (blockCount n d) → ℝ) : 0 ≤ blockMissProbability n d β B p σ θ s est U ∧ blockMissProbability n d β B p σ θ s est U ≤ 1 := by constructor · unfold blockMissProbability apply sum_nonneg intro z hz exact mul_nonneg (by rw [assignmentMass_eq_bernoulli_p n p hp0 hp1]; exact (bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1)).p_nonneg z) (missIndicator_nonneg _ θ s _) · calc blockMissProbability n d β B p σ θ s est U ≤ ∑ z : Fin n → Bool, assignmentMass n p z * 1 := by unfold blockMissProbability apply Finset.sum_le_sum intro z hz apply mul_le_mul_of_nonneg_left (missIndicator_le_one _ θ s _) rw [assignmentMass_eq_bernoulli_p n p hp0 hp1] exact (bernoulliDesign (fun _ : Fin n => p) (fun _ => hp0) (fun _ => hp1)).p_nonneg z _ = 1 := by rw [← Finset.sum_mul, sum_assignmentMass_one n p hp0 hp1] ring

lemma blockPrior_miss_sq_le_worstRisk (n d β : ℕ) (B p σ : ℝ) (hn : 1 ≤ n) (hd : 1 ≤ d) (hdn : d ≤ n) (hB : 0 < B) (hβ : 1 ≤ β) (hp0 : 0 < p) (hp1 : p < 1) (hσ : σ = -1 ∨ σ = 1) (est : Estimator (Fin n)) (hest : AdmissibleEstimator p (le_of_lt hp0) (le_of_lt hp1) d β B est) : let s := activeShare n d * tiltAmplitude B β p (blockCount n d) d s ^ 2 * (blockPriorLaw n d β B p σ).real {x | s ≤ |blockEstimatorStatistic n d est x - σ * s|} ≤ worstRisk p (le_of_lt hp0) (le_of_lt hp1) d β B est := by classical let s := activeShare n d * tiltAmplitude B β p (blockCount n d) d let q := blockMissProbability n d β B p σ (σ * s) s est let r : (Fin (blockCount n d) → ℝ) → ℝ := fun U => if blockBaselineSupport B U then s ^ 2 * q U else 0 let ν := baselineProductMeasure B (blockCount n d) let R := worstRisk p (le_of_lt hp0) (le_of_lt hp1) d β B est have hρ0 : 0 ≤ activeShare n d := by unfold activeShare positivity have hH : 0 < representerMassSup β p := representerMassSup_pos β p hβ hp0 hp1 have hδ0 : 0 ≤ tiltAmplitude B β p (blockCount n d) d := by unfold tiltAmplitude positivity have hs0 : 0 ≤ s := mul_nonneg hρ0 hδ0 have hR0 : 0 ≤ R := by let U0 : Fin (blockCount n d) → ℝ := fun _ => 0 have hU0 : blockBaselineSupport B U0 := by intro b change |(0 : ℝ)| ≤ B / 2 norm_num linarith let M0 := blockScheduleModel n d β B p σ hn hd hdn hB.le hβ hp0 hp1 hσ U0 hU0 have hr0 : 0 ≤ riskAt p (le_of_lt hp0) (le_of_lt hp1) M0 est := by unfold riskAt exact (bernoulliDesign (fun _ : Fin n => p) (fun _ => le_of_lt hp0) (fun _ => le_of_lt hp1)).mse_nonneg _ _ exact hr0.trans (le_csSup hest.2 (Set.mem_range_self M0)) have hpoint (U : Fin (blockCount n d) → ℝ) : r U ≤ R := by by_cases hU : blockBaselineSupport B U · rw [show r U = s ^ 2 * q U by simp [r, hU]] let M := blockScheduleModel n d β B p σ hn hd hdn hB.le hβ hp0 hp1 hσ U hU have hrange : riskAt p (le_of_lt hp0) (le_of_lt hp1) M est ≤ R := le_csSup hest.2 (Set.mem_range_self M) apply le_trans _ hrange unfold riskAt mse unfold q blockMissProbability rw [Finset.mul_sum] apply Finset.sum_le_sum intro z hz rw [show s ^ 2 * (assignmentMass n p z * missIndicator (blockEstimatorStatistic n d est) (σ * s) s (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z))) = assignmentMass n p z * (s ^ 2 * missIndicator (blockEstimatorStatistic n d est) (σ * s) s (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z))) by ring] rw [assignmentMass_eq_bernoulli_p n p (le_of_lt hp0) (le_of_lt hp1)] apply mul_le_mul_of_nonneg_left _ <| (bernoulliDesign (fun _ : Fin n => p) (fun _ => le_of_lt hp0) (fun _ => le_of_lt hp1)).p_nonneg z have ht : tte M.edge M.coef = σ * s := by change tte (blockGraph n d) (blockSchedule n d β B p σ hσ U) = σ * s rw [tte_blockSchedule n d β B p σ hn hd hβ hp0 hp1 hσ U] dsimp [s] ring have hobs := blockObservedVector_translate n d β B p σ hd hσ z U change s ^ 2 * missIndicator (blockEstimatorStatistic n d est) (σ * s) s (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) ≤ (est (edgeFn M) z (obsOutcome M.edge M.coef z) - tte M.edge M.coef) ^ 2 rw [ht] have hedge : edgeFn M = fun j i => decide (blockGraph n d j i) := by rfl rw [hedge] change s ^ 2 * missIndicator (blockEstimatorStatistic n d est) (σ * s) s (z, fun b => U b + σ * tiltAmplitude B β p (blockCount n d) d * blockRepresenter β p d (blockAssignment n d b z)) ≤ (est (fun j i => decide (blockGraph n d j i)) z (obsOutcome (blockGraph n d) (blockSchedule n d β B p σ hσ U) z) - σ * s) ^ 2 rw [← hobs] unfold blockEstimatorStatistic missIndicator split_ifs with he · simpa [sq_abs] using (sq_le_sq₀ hs0 (abs_nonneg _)|>.2 he) · simp positivity · simp [r, hU, hR0] have hrmeas : Measurable r := by unfold r apply Measurable.ite (measurableSet_blockBaselineSupport B _) · exact measurable_const.mul (blockMissProbability_measurable n d β B p σ (σ * s) s est hest.1) · exact measurable_const letI : IsProbabilityMeasure ν := baselineProductMeasure_isProbability B (blockCount n d) hB have hrint : Integrable r ν := by apply Integrable.of_bound hrmeas.aestronglyMeasurable |R| exact Filter.Eventually.of_forall fun U => by rw [Real.norm_eq_abs, abs_of_nonneg] · exact (hpoint U).trans (le_abs_self R) · unfold r split_ifs · exact mul_nonneg (sq_nonneg _) (blockMissProbability_bounds n d β B p σ (σ * s) s (le_of_lt hp0) (le_of_lt hp1) est U).1 · norm_num have hrbdd : BddAbove (range r) := ⟨R, by rintro _ ⟨U, rfl⟩ exact hpoint U⟩ have havg : ∫ U, r U ∂ν ≤ sSup (range r) := integral_le_sSup_range_of_isProbabilityMeasure ν r hrint hrbdd have hsup : sSup (range r) ≤ R := csSup_le (Set.range_nonempty r) (fun _ h => by rcases h with ⟨U, rfl⟩ exact hpoint U) calc s ^ 2 * (blockPriorLaw n d β B p σ).real {x | s ≤ |blockEstimatorStatistic n d est x - σ * s|} = ∫ U, r U ∂ν := by rw [blockPriorLaw_real_miss n d β B p σ (σ * s) s hB hp0 hp1 est hest.1] unfold ν baselineProductMeasure rw [integral_withDensity_eq_integral_toReal_smul₀] · rw [← integral_const_mul] apply integral_congr_ae exact Filter.Eventually.of_forall fun U => by change s ^ 2 * (baselineProductDensity B (blockCount n d) U * q U) = (ofReal (baselineProductDensity B (blockCount n d) U)).toReal * r U by_cases hU : blockBaselineSupport B U · rw [ENNReal.toReal_ofReal (baselineProductDensity_nonneg B (blockCount n d) hB U)] simp only [r, hU, if_pos] unfold q blockMissProbability ring · rw [baselineProductDensity_eq_zero_of_not_support B _ U hU] simp [r, hU] · exact (baselineProductDensity_integrable B (blockCount n d)).1.aemeasurable.ennreal_ofReal · exact Filter.Eventually.of_forall fun U => ENNReal.ofReal_lt_top _ ≤ sSup (range r) := havg _ ≤ R := hsup

lemma potentialOutcome_abs_le_mass {V : Type*} [Fintype V] [DecidableEq V] {G : V → V → Prop} {c : V → Finset V → ℝ} {B : ℝ} (hmass : BoundedCoeffMass G c B) (i : V) (z : V → Bool) : |potentialOutcome G c i z| ≤ B := by classical unfold potentialOutcome calc |∑ S ∈ (nbhd G i).powerset, c i S * ∏ j ∈ S, if z j then (1 : ℝ) else 0| ≤ ∑ S ∈ (nbhd G i).powerset, |c i S * ∏ j ∈ S, if z j then (1 : ℝ) else 0| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ S ∈ (nbhd G i).powerset, |c i S| := by apply Finset.sum_le_sum intro S hS rw [abs_mul] apply mul_le_of_le_one_right (abs_nonneg _) rw [Finset.abs_prod] exact Finset.prod_le_one (fun _ _ => abs_nonneg _) (fun j _ => by cases z j <;> norm_num) _ ≤ B := hmass i

lemma tte_abs_le_two_mul_of_modelClass {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] {d β : ℕ} {B : ℝ} (M : ModelClass V d β B) : |tte M.edge M.coef| ≤ 2 * B := by classical have hcard : (0 : ℝ) < Fintype.card V := by exact_mod_cast Fintype.card_pos unfold tte rw [abs_mul, abs_of_pos (inv_pos.mpr hcard)] calc (Fintype.card V : ℝ)⁻¹ * |∑ i : V, (potentialOutcome M.edge M.coef i (fun _ => true) - potentialOutcome M.edge M.coef i (fun _ => false))| ≤ (Fintype.card V : ℝ)⁻¹ * ∑ i : V, |potentialOutcome M.edge M.coef i (fun _ => true) - potentialOutcome M.edge M.coef i (fun _ => false)| := by gcongr exact Finset.abs_sum_le_sum_abs _ _ _ ≤ (Fintype.card V : ℝ)⁻¹ * ∑ _i : V, (2 * B) := by gcongr with i calc |_ - _| ≤ |potentialOutcome M.edge M.coef i (fun _ => true)| + |potentialOutcome M.edge M.coef i (fun _ => false)| := abs_sub _ _ _ ≤ B + B := add_le_add (potentialOutcome_abs_le_mass M.mass_le i _) (potentialOutcome_abs_le_mass M.mass_le i _) _ = 2 * B := by ring _ = 2 * B := by simp [ne_of_gt hcard]

lemma zeroEstimator_admissible {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (d β : ℕ) (B : ℝ) : AdmissibleEstimator (V := V) p hp0 hp1 d β B (fun _ _ _ => 0) := by constructor · intro G z exact measurable_const · refine ⟨4 * B ^ 2, ?_⟩ rintro _ ⟨M, rfl⟩ unfold riskAt mse simp only change (bernoulliDesign (fun _ : V => p) (fun _ => hp0) (fun _ => hp1)).E (fun _ => (0 - tte M.edge M.coef) ^ 2) ≤ 4 * B ^ 2 rw [E_const] have ht := tte_abs_le_two_mul_of_modelClass M have hB0 : 0 ≤ B := by let i := Classical.choice ‹Nonempty V› exact (sum_nonneg fun _ _ => abs_nonneg _).trans (M.mass_le i) have hsquare := (sq_le_sq₀ (abs_nonneg (tte M.edge M.coef)) (by positivity)).2 ht rw [sq_abs] at hsquare nlinarith

lemma minimaxRisk_blockPrior_lower (n d β : ℕ) (B p : ℝ) (hn : 1 ≤ n) (hd : 1 ≤ d) (hdn : d ≤ n) (hB : 0 < B) (hβ : 1 ≤ β) (hp0 : 0 < p) (hp1 : p < 1) (hhell : hellingerSqDensity (blockDominatingMeasure n d) (blockPriorDensity n d β B p 1) (blockPriorDensity n d β B p (-1)) ≤ 1 / 4) : let s := activeShare n d * tiltAmplitude B β p (blockCount n d) d s ^ 2 / 4 ≤ minimaxRisk (V := Fin n) p (le_of_lt hp0) (le_of_lt hp1) d β B := by classical let s := activeShare n d * tiltAmplitude B β p (blockCount n d) d have hs0 : 0 ≤ s := by unfold s activeShare tiltAmplitude have hH := representerMassSup_pos β p hβ hp0 hp1 positivity let Pplus := blockPriorLaw n d β B p 1 let Pminus := blockPriorLaw n d β B p (-1) letI : IsProbabilityMeasure Pplus := blockPriorLaw_isProbability n d β B p 1 hn hd hdn hB hp0 hp1 (inr rfl) letI : IsProbabilityMeasure Pminus := blockPriorLaw_isProbability n d β B p (-1) hn hd hdn hB hp0 hp1 (inl rfl) have htv0 := blockPrior_tvDist_le_sqrt_hellinger n d β B p hn hd hdn hB hp0 hp1 have htv : tvDist Pplus Pminus ≤ 1 / 2 := by apply htv0.trans calc sqrt (hellingerSqDensity (blockDominatingMeasure n d) (blockPriorDensity n d β B p 1) (blockPriorDensity n d β B p (-1))) ≤ sqrt (1 / 4) := Real.sqrt_le_sqrt hhell _ = 1 / 2 := by rw [show (1 / 4 : ℝ) = (1 / 2 : ℝ) ^ 2 by ring, Real.sqrt_sq_eq_abs] norm_num letI : Nonempty (Fin n) := ⟨⟨0, by omega⟩⟩ unfold minimaxRisk apply le_csInf · refine ⟨worstRisk (V := Fin n) p (le_of_lt hp0) (le_of_lt hp1) d β B ((fun _ _ _ => (0 : ℝ)) : Estimator (Fin n)), ?_⟩ exact ⟨(fun _ _ _ => (0 : ℝ) : Estimator (Fin n)), zeroEstimator_admissible p (le_of_lt hp0) (le_of_lt hp1) d β B, rfl⟩ · intro R hR rcases hR with ⟨est, hest, rfl⟩ let T := blockEstimatorStatistic n d est have hT : Measurable T := blockEstimatorStatistic_measurable n d est hest.1 have hsep : 2 * s ≤ |s - (-s)| := by rw [sub_neg_eq_add] rw [abs_of_nonneg (add_nonneg hs0 hs0)] ring_nf exact le_rfl have hcam := two_point_lower_bound_of_tvDist_le (P₀ := Pplus) (P₁ := Pminus) hT hsep htv have hplus := blockPrior_miss_sq_le_worstRisk n d β B p 1 hn hd hdn hB hβ hp0 hp1 (inr rfl) est hest have hminus := blockPrior_miss_sq_le_worstRisk n d β B p (-1) hn hd hdn hB hβ hp0 hp1 (inl rfl) est hest change (1 - (1 / 2 : ℝ)) / 2 ≤ max (Pplus.real {x | s ≤ |T x - s|}) (Pminus.real {x | s ≤ |T x - -s|}) at hcam dsimp only at hplus hminus simp only [one_mul] at hplus simp only [neg_one_mul] at hminus change s ^ 2 * Pplus.real {x | s ≤ |T x - s|} ≤ worstRisk p (le_of_lt hp0) (le_of_lt hp1) d β B est at hplus change s ^ 2 * Pminus.real {x | s ≤ |T x - -s|} ≤ worstRisk p (le_of_lt hp0) (le_of_lt hp1) d β B est at hminus have hmax : s ^ 2 * max (Pplus.real {x | s ≤ |T x - s|}) (Pminus.real {x | s ≤ |T x - -s|}) ≤ worstRisk p (le_of_lt hp0) (le_of_lt hp1) d β B est := by by_cases hle : Pplus.real {x | s ≤ |T x - s|} ≤ Pminus.real {x | s ≤ |T x - -s|} · rw [max_eq_right hle] exact hminus · rw [max_eq_left (le_of_not_ge hle)] exact hplus have hquarter : (1 / 4 : ℝ) ≤ max (Pplus.real {x | s ≤ |T x - s|}) (Pminus.real {x | s ≤ |T x - -s|}) := by convert hcam using 1 <;> norm_num nlinarith [mul_le_mul_of_nonneg_left hquarter (sq_nonneg s)]

lemma tte_abs_le_of_modelClass {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] {d β : ℕ} {B : ℝ} (M : ModelClass V d β B) : |tte M.edge M.coef| ≤ B := by classical have hn : (0 : ℝ) < Fintype.card V := by exact_mod_cast Fintype.card_pos unfold tte rw [abs_mul, abs_of_pos (inv_pos.mpr hn)] calc (Fintype.card V : ℝ)⁻¹ * |∑ i : V, (potentialOutcome M.edge M.coef i (fun _ => true) - potentialOutcome M.edge M.coef i (fun _ => false))| ≤ (Fintype.card V : ℝ)⁻¹ * ∑ i : V, |potentialOutcome M.edge M.coef i (fun _ => true) - potentialOutcome M.edge M.coef i (fun _ => false)| := by gcongr exact Finset.abs_sum_le_sum_abs _ _ _ ≤ (Fintype.card V : ℝ)⁻¹ * ∑ _i : V, B := by gcongr with i have htrue : potentialOutcome M.edge M.coef i (fun _ => true) = ∑ S ∈ (nbhd M.edge i).powerset, M.coef i S := by simp [potentialOutcome] have hfalse : potentialOutcome M.edge M.coef i (fun _ => false) = M.coef i ∅ := by unfold potentialOutcome simp_rw [Finset.prod_const] rw [Finset.sum_eq_single ∅] · simp · intro S hS hS0 have hcard : 0 < S.card := Finset.card_pos.mpr (Finset.nonempty_iff_ne_empty.mpr hS0) simp only [Bool.false_eq_true, ↓reduceIte] rw [zero_pow (Nat.ne_of_gt hcard), mul_zero] · simp rw [htrue, hfalse] rw [show (∑ S ∈ (nbhd M.edge i).powerset, M.coef i S) - M.coef i ∅ = ∑ S ∈ (nbhd M.edge i).powerset, if S = ∅ then 0 else M.coef i S by rw [show M.coef i ∅ = ∑ S ∈ (nbhd M.edge i).powerset, if S = ∅ then M.coef i ∅ else 0 by simp] rw [← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro S hS by_cases hS0 : S = ∅ · subst S simp · have hSne : S.Nonempty := Finset.nonempty_iff_ne_empty.mpr hS0 simp [hS0, hSne]] calc |∑ S ∈ (nbhd M.edge i).powerset, if S = ∅ then 0 else M.coef i S| ≤ ∑ S ∈ (nbhd M.edge i).powerset, |if S = ∅ then 0 else M.coef i S| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ S ∈ (nbhd M.edge i).powerset, |M.coef i S| := by apply Finset.sum_le_sum intro S hS split_ifs <;> simp _ ≤ B := M.mass_le i _ = B := by simp [hn.ne']

lemma tte_abs_le_of_bddModelClass {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] {d β : ℕ} {B : ℝ} (M : BddOutcomeModelClass V d β B) : |tte M.edge M.coef| ≤ 2 * B := by classical have hn : (0 : ℝ) < Fintype.card V := by exact_mod_cast Fintype.card_pos unfold tte rw [abs_mul, abs_of_pos (inv_pos.mpr hn)] calc (Fintype.card V : ℝ)⁻¹ * |∑ i : V, (_ - _)| ≤ (Fintype.card V : ℝ)⁻¹ * ∑ i : V, |potentialOutcome M.edge M.coef i (fun _ => true) - potentialOutcome M.edge M.coef i (fun _ => false)| := by gcongr exact Finset.abs_sum_le_sum_abs _ _ _ ≤ (Fintype.card V : ℝ)⁻¹ * ∑ _i : V, (2 * B) := by gcongr with i exact (abs_sub _ _).trans <| (add_le_add (M.outcome_bound i _) (M.outcome_bound i _)).trans_eq (by ring) _ = 2 * B := by simp [hn.ne']

lemma clipTo_sq_sub_le (R x t : ℝ) (hR : 0 ≤ R) (ht : |t| ≤ R) : (clipTo R x - t) ^ 2 ≤ (x - t) ^ 2 := by rw [abs_le] at ht unfold clipTo by_cases hxlo : x < -R · rw [min_eq_right (le_trans hxlo.le (neg_le_self hR)), max_eq_left hxlo.le] nlinarith · have hxlo' : -R ≤ x := le_of_not_gt hxlo by_cases hxhi : R < x · rw [min_eq_left hxhi.le, max_eq_right (by linarith)] nlinarith · rw [min_eq_right (le_of_not_gt hxhi), max_eq_right hxlo']

lemma riskAt_clipped_le_raw {V : Type*} [Fintype V] [DecidableEq V] [Nonempty V] (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {d β : ℕ} {B : ℝ} (hB : 0 ≤ B) (M : ModelClass V d β B) : riskAt p hp0 hp1 M (snipeClipped B β p) ≤ riskAt p hp0 hp1 M (snipeEstimator β p) := by unfold riskAt FiniteDesign.mse FiniteDesign.E apply Finset.sum_le_sum intro z hz apply mul_le_mul_of_nonneg_left _ <| (bernoulliDesign (fun _ : V => p) (fun _ => hp0) (fun _ => hp1)).p_nonneg z exact clipTo_sq_sub_le B _ _ hB (tte_abs_le_of_modelClass M)