Experimentation.Two­Stage­Interference.Asymptotic

lemma DEbar_eq_of_homogeneous (h : Homogeneous Exp t stud δ M v) (n : ℕ) : (Exp n).DEbar = δ := by simp only [LHExperiment.DEbar, CE_direct, popMean, ← sub_div, ← Finset.sum_sub_distrib] rw [Finset.sum_congr rfl (fun i _ => h.hδ n i), Finset.sum_const, Finset.card_univ, nsmul_eq_mul] rw [mul_comm, mul_div_assoc, div_self (Exp n).hN, mul_one]

lemma directVar_eq_of_homogeneous (h : Homogeneous Exp t stud δ M v) (n : ℕ) : (Exp n).directVar = v n / (Exp n).C := by have hSmu : SmuVar (fun i => groupMean (Exp n).ψ (Exp n).Y i true - groupMean (Exp n).ψ (Exp n).Y i false) = 0 := by simp only [SmuVar] have hmubar : (∑ i, (groupMean (Exp n).ψ (Exp n).Y i true - groupMean (Exp n).ψ (Exp n).Y i false)) / (card (Exp n).ι : ℝ) = δ := by rw [Finset.sum_congr rfl (fun i _ => h.hδ n i), Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_comm, mul_div_assoc, div_self (Exp n).hN, mul_one] rw [hmubar] rw [Finset.sum_congr rfl (fun i _ => by rw [h.hδ n i, sub_self]; ring : ∀ i ∈ univ, (groupMean (Exp n).ψ (Exp n).Y i true - groupMean (Exp n).ψ (Exp n).Y i false - δ) ^ 2 = 0)] simp have hwithin : ∑ i, ((Exp n).ψ i).Var (fun w => groupEst (Exp n).Y i true ((Exp n).m1 i) w - groupEst (Exp n).Y i false ((Exp n).m0 i) w) = (card (Exp n).ι : ℝ) * v n := by rw [show (∑ i, ((Exp n).ψ i).Var (fun w => groupEst (Exp n).Y i true ((Exp n).m1 i) w - groupEst (Exp n).Y i false ((Exp n).m0 i) w)) = ∑ i, ((Exp n).ψ i).Var (groupDiff (Exp n) i) from rfl, Finset.sum_congr rfl (fun i _ => h.hv n i), Finset.sum_const, Finset.card_univ, nsmul_eq_mul] simp only [LHExperiment.directVar] rw [hSmu, hwithin] have hC := (Exp n).hC have hN := (Exp n).hN field_simp ring

lemma stud_eq_sum_of_homogeneous (h : Homogeneous Exp t stud δ M v) (n : ℕ) (s : StratAssign (Exp n).ι) (hs : (Exp n).D₁.p s ≠ 0) (w : ∀ i, Fin ((Exp n).gsize i) → Bool) : stud n (s, w) = ∑ i, cltSummand n δ v s i (w i) := by have hCpos : 0 < (Exp n).C := by rcases lt_or_gt_of_ne (Exp n).hC with h0 | h0 · -- if C < 0, contradiction with hcount (sum of indicators ≥ 0) exfalso have hnn : (0 : ℝ) ≤ ∑ i, if s i then (1 : ℝ) else 0 := sum_nonneg (fun i _ => by positivity) rw [h.hcount n s hs] at hnn linarith · exact h0 have hvpos := h.hvpos n have hcount := h.hcount n s hs -- `√(C·v) > 0` and `C·√(v/C) = √(C·v)`. have hCv : (0 : ℝ) < (Exp n).C * v n := mul_pos hCpos hvpos have hsqrtCv : 0 < sqrt ((Exp n).C * v n) := Real.sqrt_pos.mpr hCv have hsqrtvC : 0 < sqrt (v n / (Exp n).C) := Real.sqrt_pos.mpr (div_pos hvpos hCpos) have hkey : (Exp n).C * sqrt (v n / (Exp n).C) = sqrt ((Exp n).C * v n) := by rw [show (Exp n).C * v n = (Exp n).C ^ 2 * (v n / (Exp n).C) by field_simp, Real.sqrt_mul (by positivity), Real.sqrt_sq hCpos.le] rw [h.hstud, estD_eq_agg, DEbar_eq_of_homogeneous h, directVar_eq_of_homogeneous h] -- Recenter: `(∑ 1(sᵢ)·dᵢ)/C − δ = (∑ 1(sᵢ)·(dᵢ−δ))/C` using `∑ 1(sᵢ) = C`. have hrecenter : (∑ i, (if s i then (1 : ℝ) else 0) * groupDiff (Exp n) i (w i)) / (Exp n).C - δ = (∑ i, (if s i then (1 : ℝ) else 0) * (groupDiff (Exp n) i (w i) - δ)) / (Exp n).C := by rw [Finset.sum_congr rfl (fun i _ => mul_sub _ _ _ : ∀ i ∈ univ, (if s i then (1:ℝ) else 0) * (groupDiff (Exp n) i (w i) - δ) = (if s i then (1:ℝ) else 0) * groupDiff (Exp n) i (w i) - (if s i then (1:ℝ) else 0) * δ), Finset.sum_sub_distrib, ← Finset.sum_mul, hcount, sub_div, mul_div_cancel_left₀ _ (ne_of_gt hCpos)] rw [hrecenter] -- Distribute the scalar `1/(C·√(v/C)) = 1/√(C·v)` into the sum. simp only [cltSummand] rw [div_div, hkey, Finset.sum_div]

theorem directEffect_clt (Exp : ℕ → LHExperiment) (t : ℝ) (stud : ∀ n, (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → ℝ) (_hstud : ∀ n sw, stud n sw = ((Exp n).estD sw - (Exp n).DEbar) / sqrt ((Exp n).directVar)) (cond : ∀ n, StratAssign (Exp n).ι → FiniteDesign (∀ i, Fin ((Exp n).gsize i) → Bool)) (hcondDef : ∀ n s, cond n s = prodDesign (fun i => if s i then (Exp n).ψ i else (Exp n).φ i)) (hcond : ∃ B, Tendsto B atTop (𝓝 0) ∧ ∀ n s, |(cond n s).Pr (fun w => stud n (s, w) ≤ t) - stdNormalCdf t| ≤ B n) : Tendsto (fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ t)) atTop (𝓝 (stdNormalCdf t)) := by obtain ⟨B, hB, hbound⟩ := hcond -- Rewrite each unconditional CDF as the stage-1 average of conditional CDFs. have hrw : ∀ n, (Exp n).jointD.Pr (fun sw => stud n sw ≤ t) = (Exp n).D₁.E (fun s => (cond n s).Pr (fun w => stud n (s, w) ≤ t)) := by intro n rw [LHExperiment.jointD, jointDesign, FiniteDesign.Pr_compound_eq_E_condPr] apply (Exp n).D₁.E_congr intro s rw [hcondDef n s] simp_rw [hrw] -- Apply the mixture-lifting lemma with `F n s := (cond n s).Pr (…)`, `L := Φ(t)`, bound `B`. exact FiniteDesign.tendsto_E_of_uniformBound (fun n => (Exp n).D₁) (fun n s => (cond n s).Pr (fun w => stud n (s, w) ≤ t)) (stdNormalCdf t) B hbound hB

theorem directEffect_clt_homogeneous (h : Homogeneous Exp t stud δ M v) : Tendsto (fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ t)) atTop (𝓝 (stdNormalCdf t)) := by -- Reference-selection conditional CDF and its distance to `Φ(t)`. set F : ∀ n, StratAssign (Exp n).ι → ℝ := fun n s => (condDesign (Exp n) s).Pr (fun w => stud n (s, w) ≤ t) with hF set B : ℕ → ℝ := fun n => |F n (refSel Exp n) - stdNormalCdf t| with hBdef -- `B n → 0` since the reference conditional CDF converges to `Φ(t)`. have hB : Tendsto B atTop (𝓝 0) := by have hc := condCLT_ref h rw [tendsto_iff_norm_sub_tendsto_zero] at hc simpa only [hBdef, hF, Real.norm_eq_abs] using hc -- Rewrite each joint CDF as the stage-1 average of conditional CDFs. have hrw : ∀ n, (Exp n).jointD.Pr (fun sw => stud n sw ≤ t) = (Exp n).D₁.E (F n) := by intro n rw [LHExperiment.jointD, jointDesign, FiniteDesign.Pr_compound_eq_E_condPr] apply (Exp n).D₁.E_congr intro s rw [hF] rfl simp_rw [hrw] -- Average via the support-restricted mixture-lifting lemma. refine FiniteDesign.tendsto_E_of_uniformBound_ae (fun n => (Exp n).D₁) F (stdNormalCdf t) B (fun n s hs => ?_) hB -- On the support, `hhom` identifies `F n s` with `F n (refSel)`. simp only [hBdef, hF] rw [h.hhom n s (refSel Exp n) hs (refSel_mem Exp n)]

theorem estDirect_consistent (Exp : ℕ → LHExperiment) (hVar0 : Tendsto (fun n => (Exp n).directVar) atTop (𝓝 0)) {ε : ℝ} (hε : 0 < ε) : Tendsto (fun n => (Exp n).jointD.Pr (fun sw => ε ≤ |(Exp n).estD sw - (Exp n).DEbar|)) atTop (𝓝 0) := by refine squeeze_zero (g := fun n => (Exp n).directVar / ε ^ 2) (fun n => ?_) (fun n => ?_) ?_ · -- `0 ≤ Pr_n`: a probability is nonnegative. exact (Exp n).jointD.Pr_nonneg _ · -- `Pr_n ≤ directVar_n / ε²` by Chebyshev, recentering via unbiasedness. have hcenter : (Exp n).DEbar = (Exp n).jointD.E (Exp n).estD := ((Exp n).E_estD).symm change (Exp n).jointD.Pr (fun sw => ε ≤ |(Exp n).estD sw - (Exp n).DEbar|) ≤ (Exp n).directVar / ε ^ 2 rw [hcenter, ← (Exp n).var_estD] exact (Exp n).jointD.chebyshev (Exp n).estD hε · -- `directVar_n / ε² → 0 / ε² = 0`. simpa using hVar0.div_const (ε ^ 2)

theorem directEffect_clt_identical (R : ℕ → IdenticalRef) (t δ M : ℝ) (hδ : ∀ n, (R n).refDelta = δ) (hvpos : ∀ n, 0 < (R n).refVar) (hMbound : ∀ n i w, |groupDiff (R n).toExp i w - δ| ≤ M) (hcount : ∀ n s, (R n).toExp.D₁.p s ≠ 0 → (∑ i, if s i then (1 : ℝ) else 0) = (R n).toExp.C) (hB0 : Tendsto (fun n => M / sqrt ((R n).toExp.C * (R n).refVar)) atTop (𝓝 0)) (hNB3 : Tendsto (fun n => (card (R n).toExp.ι : ℝ) * (M / sqrt ((R n).toExp.C * (R n).refVar)) ^ 3) atTop (𝓝 0)) : Tendsto (fun n => (R n).toExp.jointD.Pr (fun sw => (R n).studId sw ≤ t)) atTop (𝓝 (stdNormalCdf t)) := directEffect_clt_homogeneous (homogeneous_of_identical R t δ M hδ hvpos hMbound hcount hB0 hNB3)

theorem wald_coverage_oracle (Exp : ℕ → LHExperiment) (stud : ∀ n, (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → ℝ) (hstud : ∀ n sw, stud n sw = ((Exp n).estD sw - (Exp n).DEbar) / sqrt ((Exp n).directVar)) (hVar : ∀ n, 0 < (Exp n).directVar) {γ : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - γ / 2) (hcltPos : Tendsto (fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ zq)) atTop (𝓝 (stdNormalCdf zq))) (hcltNeg : Tendsto (fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ -zq)) atTop (𝓝 (stdNormalCdf (-zq)))) : 1 - γ ≤ liminf (fun n => (Exp n).jointD.Pr (fun sw => |(Exp n).estD sw - (Exp n).DEbar| ≤ zq * sqrt ((Exp n).directVar))) atTop := by -- The studentized lower-CDF probabilities at `zq` and `-zq`. set S : ℕ → ℝ := fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ zq) with hSdef set Lo : ℕ → ℝ := fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ -zq) with hLodef set I : ℕ → ℝ := fun n => (Exp n).jointD.Pr (fun sw => |(Exp n).estD sw - (Exp n).DEbar| ≤ zq * sqrt ((Exp n).directVar)) with hIdef -- (1) Limit of `S - Lo`. have hlim : Tendsto (fun n => S n - Lo n) atTop (𝓝 (1 - γ)) := by have h := hcltPos.sub hcltNeg rw [stdNormalCdf_neg zq, hzq] at h have he : (1 - γ / 2) - (1 - (1 - γ / 2)) = 1 - γ := by ring rwa [he] at h -- (2) Pointwise lower bound `S - Lo ≤ I`. have hbound : ∀ n, S n - Lo n ≤ I n := by intro n -- Abbreviate the studentized statistic and the square-root denominator. set W : (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → ℝ := fun sw => stud n sw with hWdef -- Split `S` by the event `W ≤ -zq`. have hsplit := (Exp n).jointD.Pr_split (fun sw => W sw ≤ zq) (fun sw => W sw ≤ -zq) -- The first piece equals `Lo`. have hfirst : (Exp n).jointD.Pr (fun sw => W sw ≤ zq ∧ W sw ≤ -zq) = Lo n := by apply (Exp n).jointD.Pr_congr intro sw constructor · exact fun h => h.2 · intro h2 exact ⟨le_trans h2 (by linarith [hzq0]), h2⟩ -- So `S - Lo` is the probability of the second piece. have hSLo : S n - Lo n = (Exp n).jointD.Pr (fun sw => W sw ≤ zq ∧ ¬ W sw ≤ -zq) := by have : S n = (Exp n).jointD.Pr (fun sw => W sw ≤ zq ∧ W sw ≤ -zq) + (Exp n).jointD.Pr (fun sw => W sw ≤ zq ∧ ¬ W sw ≤ -zq) := hsplit rw [this, hfirst]; ring rw [hSLo] -- That second piece is contained in `I`'s event. apply (Exp n).jointD.Pr_mono intro sw hz obtain ⟨hz1, hz2⟩ := hz rw [not_le] at hz2 -- `|W sw| ≤ zq`. have habs : |W sw| ≤ zq := abs_le.mpr ⟨le_of_lt hz2, hz1⟩ -- Unfold the studentized statistic. set s : ℝ := sqrt ((Exp n).directVar) with hsdef have hs : 0 < s := Real.sqrt_pos.mpr (hVar n) rw [hWdef] at habs simp only at habs rw [hstud n sw, ← hsdef] at habs rw [abs_div, abs_of_pos hs, div_le_iff₀ hs] at habs exact habs -- (3) Conclude with liminf. have hbdd : IsBoundedUnder (· ≥ ·) atTop (fun n => S n - Lo n) := hlim.isBoundedUnder_ge have hcobdd : IsCoboundedUnder (· ≥ ·) atTop I := isCoboundedUnder_ge_of_le atTop (x := (1 : ℝ)) (fun n => (Exp n).jointD.Pr_le_one _) calc 1 - γ = liminf (fun n => S n - Lo n) atTop := hlim.liminf_eq.symm _ ≤ liminf I atTop := Filter.liminf_le_liminf (Filter.Eventually.of_forall hbound) hbdd hcobdd

theorem wald_coverage_feasible (Exp : ℕ → LHExperiment) (stud : ∀ n, (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → ℝ) (hstud : ∀ n sw, stud n sw = ((Exp n).estD sw - (Exp n).DEbar) / Real.sqrt ((Exp n).directVar)) (Vh : ∀ n, (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → ℝ) (hclt : ∀ t, Tendsto (fun n => (Exp n).jointD.Pr (fun sw => stud n sw ≤ t)) atTop (𝓝 (stdNormalCdf t))) (hVar : ∀ n, 0 < (Exp n).directVar) (hVhat : ∀ ε : ℝ, 0 < ε → Tendsto (fun n => (Exp n).jointD.Pr (fun sw => Vh n sw < (1 - ε) * (Exp n).directVar)) atTop (𝓝 0)) {γ : ℝ} (zq : ℝ) (hzq0 : 0 ≤ zq) (hzq : stdNormalCdf zq = 1 - γ / 2) : 1 - γ ≤ liminf (fun n => (Exp n).jointD.Pr (fun sw => |(Exp n).estD sw - (Exp n).DEbar| ≤ zq * Real.sqrt (Vh n sw))) atTop := by -- The coverage probability sequence. set I : ℕ → ℝ := fun n => (Exp n).jointD.Pr (fun sw => |(Exp n).estD sw - (Exp n).DEbar| ≤ zq * Real.sqrt (Vh n sw)) with hIdef -- `I` is coboundedly below (always ≤ 1). have hIcobdd : IsCoboundedUnder (· ≥ ·) atTop I := isCoboundedUnder_ge_of_le atTop (x := (1 : ℝ)) (fun n => (Exp n).jointD.Pr_le_one _) -- For each `ε ∈ (0,1)`, `liminf I ≥ 2·Φ(zq·√(1-ε)) - 1`. have key : ∀ ε : ℝ, 0 < ε → ε < 1 → 2 * stdNormalCdf (zq * Real.sqrt (1 - ε)) - 1 ≤ liminf I atTop := by intro ε hε0 hε1 set c : ℝ := zq * Real.sqrt (1 - ε) with hcdef have h1mε : (0 : ℝ) < 1 - ε := by linarith have hc0 : 0 ≤ c := mul_nonneg hzq0 (Real.sqrt_nonneg _) -- The CLT band probability and the "bad variance" probability. set B : ℕ → ℝ := fun n => (Exp n).jointD.Pr (fun sw => -c ≤ stud n sw ∧ stud n sw ≤ c) with hBdef set A : ℕ → ℝ := fun n => (Exp n).jointD.Pr (fun sw => Vh n sw < (1 - ε) * (Exp n).directVar) with hAdef have hA0 : Tendsto A atTop (𝓝 0) := hVhat ε hε0 -- STEP 2: pointwise `B n - A n ≤ I n`. have hstep2 : ∀ n, B n - A n ≤ I n := by intro n set Vr : ℝ := (Exp n).directVar with hVrdef set σ : ℝ := Real.sqrt Vr with hσdef have hσpos : 0 < σ := Real.sqrt_pos.mpr (hVar n) set W : (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → ℝ := fun sw => stud n sw with hWdef -- Split `B` by the bad-variance event. set Abad : (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → Prop := fun sw => Vh n sw < (1 - ε) * Vr with hAbaddef set Bev : (StratAssign (Exp n).ι × ∀ i, Fin ((Exp n).gsize i) → Bool) → Prop := fun sw => -c ≤ W sw ∧ W sw ≤ c with hBevdef have hsplit := (Exp n).jointD.Pr_split Bev Abad -- `Pr(Bev ∧ Abad) ≤ A n`. have hBA : (Exp n).jointD.Pr (fun sw => Bev sw ∧ Abad sw) ≤ A n := by apply (Exp n).jointD.Pr_mono; intro sw hz; exact hz.2 -- So `B n - A n ≤ Pr(Bev ∧ ¬Abad)`. have hBmA : B n - A n ≤ (Exp n).jointD.Pr (fun sw => Bev sw ∧ ¬ Abad sw) := by have hBeq : B n = (Exp n).jointD.Pr (fun sw => Bev sw ∧ Abad sw) + (Exp n).jointD.Pr (fun sw => Bev sw ∧ ¬ Abad sw) := hsplit linarith [hBeq, hBA] refine le_trans hBmA ?_ -- `Pr(Bev ∧ ¬Abad) ≤ I n` by event inclusion. apply (Exp n).jointD.Pr_mono intro sw hz obtain ⟨⟨hzlo, hzhi⟩, hznotbad⟩ := hz rw [hAbaddef, not_lt] at hznotbad -- `|W sw| ≤ c`. have habsW : |W sw| ≤ c := abs_le.mpr ⟨hzlo, hzhi⟩ -- `estD - DEbar = W sw * σ`. have hWσ : (Exp n).estD sw - (Exp n).DEbar = W sw * σ := by change (Exp n).estD sw - (Exp n).DEbar = stud n sw * σ rw [hstud n sw, ← hVrdef, ← hσdef] field_simp rw [hWσ, abs_mul, abs_of_pos hσpos] -- `|W sw| * σ ≤ c * σ = zq * √((1-ε)*Vr) ≤ zq * √(V̂)`. calc |W sw| * σ ≤ c * σ := by apply mul_le_mul_of_nonneg_right habsW hσpos.le _ = zq * Real.sqrt ((1 - ε) * Vr) := by rw [hcdef, hσdef, mul_assoc, ← Real.sqrt_mul h1mε.le] _ ≤ zq * Real.sqrt (Vh n sw) := by apply mul_le_mul_of_nonneg_left _ hzq0 exact Real.sqrt_le_sqrt hznotbad -- STEP 3: liminf chain. -- `liminf B ≤ liminf (B - A)` since `A → 0`. have hBAliminf : liminf B atTop ≤ liminf (fun n => B n - A n) atTop := by have hnegA : Tendsto (fun n => -A n) atTop (𝓝 0) := by simpa using hA0.neg have hBbdd_ge : IsBoundedUnder (· ≥ ·) atTop B := isBoundedUnder_of ⟨0, fun n => (Exp n).jointD.Pr_nonneg _⟩ have hBbdd_le : IsBoundedUnder (· ≤ ·) atTop B := isBoundedUnder_of ⟨1, fun n => (Exp n).jointD.Pr_le_one _⟩ have hnegAbdd_ge : IsBoundedUnder (· ≥ ·) atTop (fun n => -A n) := hnegA.isBoundedUnder_ge have hnegAcobdd : IsCoboundedUnder (· ≥ ·) atTop (fun n => -A n) := hnegA.isBoundedUnder_le.isCoboundedUnder_ge have h := le_liminf_add (u := B) (v := fun n => -A n) hBbdd_ge hBbdd_le hnegAbdd_ge hnegAcobdd rw [hnegA.liminf_eq] at h simp only [add_zero] at h have hsub : (B + fun n => -A n) = fun n => B n - A n := by funext n; simp [sub_eq_add_neg] rwa [hsub] at h -- `liminf (B - A) ≤ liminf I` by pointwise bound. have hABI : liminf (fun n => B n - A n) atTop ≤ liminf I atTop := by have hBAbelow : IsBoundedUnder (· ≥ ·) atTop (fun n => B n - A n) := by refine isBoundedUnder_of ⟨-1, fun n => ?_⟩ have hBn : 0 ≤ B n := by rw [hBdef]; exact (Exp n).jointD.Pr_nonneg _ have hAn : A n ≤ 1 := by rw [hAdef]; exact (Exp n).jointD.Pr_le_one _ change (-1 : ℝ) ≤ B n - A n linarith exact Filter.liminf_le_liminf (Filter.Eventually.of_forall hstep2) hBAbelow hIcobdd -- STEP 1 gives `Φ(c) - Φ(-c) ≤ liminf B`. have hstep1 := clt_interval_liminf_lb Exp stud hclt c hc0 -- Chain and rewrite `Φ(c) - Φ(-c) = 2·Φ(c) - 1`. have hΦ : stdNormalCdf c - stdNormalCdf (-c) = 2 * stdNormalCdf c - 1 := by rw [stdNormalCdf_neg c]; ring calc 2 * stdNormalCdf (zq * Real.sqrt (1 - ε)) - 1 = stdNormalCdf c - stdNormalCdf (-c) := by rw [hcdef, hΦ] _ ≤ liminf B atTop := hstep1 _ ≤ liminf (fun n => B n - A n) atTop := hBAliminf _ ≤ liminf I atTop := hABI -- STEP 4: let `ε → 0⁺` along `ε = 1/(k+1)`. The RHS bound tends to `1 - γ`. set g : ℝ → ℝ := fun ε => 2 * stdNormalCdf (zq * Real.sqrt (1 - ε)) - 1 with hgdef have hgcont : Tendsto g (𝓝 0) (𝓝 (1 - γ)) := by have hsqrt : Tendsto (fun ε : ℝ => Real.sqrt (1 - ε)) (𝓝 0) (𝓝 1) := by have : Tendsto (fun ε : ℝ => (1 - ε)) (𝓝 0) (𝓝 (1 - 0)) := (tendsto_const_nhds.sub tendsto_id) rw [sub_zero] at this have hc := (Real.continuous_sqrt.tendsto (1 : ℝ)).comp this rw [Real.sqrt_one] at hc exact hc have hzqsqrt : Tendsto (fun ε : ℝ => zq * Real.sqrt (1 - ε)) (𝓝 0) (𝓝 zq) := by have := tendsto_const_nhds (x := zq) |>.mul hsqrt simpa using this have hΦc : Tendsto (fun ε : ℝ => stdNormalCdf (zq * Real.sqrt (1 - ε))) (𝓝 0) (𝓝 (stdNormalCdf zq)) := (continuous_stdNormalCdf.tendsto zq).comp hzqsqrt have : Tendsto g (𝓝 0) (𝓝 (2 * stdNormalCdf zq - 1)) := by rw [hgdef] exact (tendsto_const_nhds.mul hΦc).sub tendsto_const_nhds have heq : 2 * stdNormalCdf zq - 1 = 1 - γ := by rw [hzq]; ring rwa [heq] at this -- Evaluate along `ε_k = 1/(k+1) → 0`, eventually in `(0,1)`. have hseq : Tendsto (fun k : ℕ => (1 : ℝ) / (k + 1)) atTop (𝓝 0) := tendsto_one_div_add_atTop_nhds_zero_nat have hgseq : Tendsto (fun k : ℕ => g (1 / (k + 1))) atTop (𝓝 (1 - γ)) := hgcont.comp hseq -- `g (1/(k+1)) ≤ liminf I` eventually (for `k ≥ 1`, so `1/(k+1) ≤ 1/2 < 1`). have hev : ∀ᶠ k : ℕ in atTop, g (1 / (k + 1)) ≤ liminf I atTop := by rw [Filter.eventually_atTop] refine ⟨1, fun k hk => ?_⟩ have hk1 : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk have hden : (0 : ℝ) < (k : ℝ) + 1 := by linarith have hpos : (0 : ℝ) < 1 / (k + 1) := by positivity have hlt1 : (1 : ℝ) / (k + 1) < 1 := by rw [div_lt_one hden]; linarith exact key _ hpos hlt1 exact le_of_tendsto hgseq hev