Paper-scale L² good event

This file packages the quantitative last step of paper §3.4, Step 1. The analytic estimates (3.31)--(3.32) must supply a factorized parametrix Q and its two operator remainders. On the paper-scale event

‖Q‖ ≤ ε⁻¹⁴, ‖Rleft‖ + ‖Rright‖ ≤ ε²⁸,

the two-sided algebra from L2ParametrixInverse.lean constructs the inverse of 1 - G M. Since ‖G‖ ≤ 1, its inverse Green operator differs from QG by at most ε¹² for sufficiently small positive ε.

The event is kept separate from its probabilistic estimate: the moment bounds in P-3.5/P-err provide the hypotheses of the Markov lemmas below.

Fourier matrix coefficients and the (3.30) bound

noncomputable def Anderson4D.torusFourierMatrixCoeff (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (α β : Z4) : ℂ

The (3.23)-signed Fourier matrix coefficient of a bounded operator. The minus sign on the left mode is the one forced by the paper's non-conjugated Fourier kernel convention.

Equations

• Anderson4D.torusFourierMatrixCoeff A α β = inner ℂ (Anderson4D.torusFourierBasis (-α)) (A (Anderson4D.torusFourierBasis β))

theorem Anderson4D.tsum_norm_sq_inner_torusFourierBasis (x : ↥TorusL2) : ∑' (k : Z4), ‖inner ℂ (torusFourierBasis k) x‖ ^ 2 = ‖x‖ ^ 2

Parseval in squared-norm form for the torus Hilbert basis.

theorem Anderson4D.tsum_norm_sq_torusFourierMatrixCoeff (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (β : Z4) : ∑' (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2 = ‖A (torusFourierBasis β)‖ ^ 2

Parseval with the left Fourier index written in the paper's -α convention.

theorem Anderson4D.operatorNormSq_le_tsum_normSq_torusFourierBasis (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (hsum : Summable fun (k : Z4) => ‖A (torusFourierBasis k)‖ ^ 2) : ‖A‖ ^ 2 ≤ ∑' (k : Z4), ‖A (torusFourierBasis k)‖ ^ 2

A bounded operator is controlled by the square-sum of its values on the torus Fourier basis. This is the Hilbert-space core of (3.30), proved directly because no named Hilbert--Schmidt API is required.

theorem Anderson4D.operatorNormSq_le_tsum_tsum_fourierMatrixCoeff (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (hsum : Summable fun (β : Z4) => ∑' (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2) : ‖A‖ ^ 2 ≤ ∑' (β : Z4) (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2

Direct Fourier double-sum form of the unweighted part of paper (3.30).

theorem Anderson4D.operatorNormSq_le_weighted_fourierMatrixCoeff (A : ↥TorusL2 →L[ℂ] ↥TorusL2) (weight : Z4 → Z4 → ℝ) (hweight : ∀ (α β : Z4), 1 ≤ weight α β) (hinner : ∀ (β : Z4), Summable fun (α : Z4) => ‖torusFourierMatrixCoeff A α β‖ ^ 2 * weight α β) (houter : Summable fun (β : Z4) => ∑' (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2 * weight α β) : ‖A‖ ^ 2 ≤ ∑' (β : Z4) (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2 * weight α β

Weighted Fourier double-sum form of (3.30). Any nonnegative weight bounded below by one may be used; the paper later instantiates this with ε⁻⁸ ⟨ε²(α+β)⟩⁶. The two summability hypotheses are the honest non-junk conditions for the nested real tsum.

noncomputable def Anderson4D.paperL2FourierWeight (ε : ℝ) (α β : Z4) : ℝ

The exact weight printed in paper (3.30): ε⁻⁸ ⟨ε²(α+β)⟩⁶. The Japanese bracket is expanded as ⟨t⟩⁶ = (1 + ‖t‖²)³, avoiding fractional powers.

Equations

• Anderson4D.paperL2FourierWeight ε α β = ε⁻¹ ^ 8 * (1 + (ε ^ 2 * ‖Anderson4D.z4EuclideanFrequency (α + β)‖) ^ 2) ^ 3

theorem Anderson4D.paperL2FourierWeight_nonneg (ε : ℝ) (α β : Z4) : 0 ≤ paperL2FourierWeight ε α β

theorem Anderson4D.one_le_paperL2FourierWeight {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (α β : Z4) : 1 ≤ paperL2FourierWeight ε α β

theorem Anderson4D.operatorNormSq_le_paperL2FourierWeight (A : ↥TorusL2 →L[ℂ] ↥TorusL2) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (hinner : ∀ (β : Z4), Summable fun (α : Z4) => ‖torusFourierMatrixCoeff A α β‖ ^ 2 * paperL2FourierWeight ε α β) (houter : Summable fun (β : Z4) => ∑' (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2 * paperL2FourierWeight ε α β) : ‖A‖ ^ 2 ≤ ∑' (β : Z4) (α : Z4), ‖torusFourierMatrixCoeff A α β‖ ^ 2 * paperL2FourierWeight ε α β

Exact paper-weight specialization of (3.30).

theorem Anderson4D.operatorNormSq_le_paperL2FourierWeight_prod (A : ↥TorusL2 →L[ℂ] ↥TorusL2) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (hsum : Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff A p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) : ‖A‖ ^ 2 ≤ ∑' (p : Z4 × Z4), ‖torusFourierMatrixCoeff A p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1

Product-index version of the exact paper-weight bound. This is the convenient form for Tonelli: one summability hypothesis replaces the two nested non-junk hypotheses.

theorem Anderson4D.lintegral_operatorNormSq_le_paperL2FourierWeight {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (A : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (hmeas : ∀ (p : Z4 × Z4), AEMeasurable (fun (ω : Ω) => ENNReal.ofReal (‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1)) μ) (hsum : ∀ᵐ (ω : Ω) ∂μ, Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) : ∫⁻ (ω : Ω), ENNReal.ofReal (‖A ω‖ ^ 2) ∂μ ≤ ∑' (p : Z4 × Z4), ∫⁻ (ω : Ω), ENNReal.ofReal (‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) ∂μ

Tonelli form of the expected (3.30) estimate. It needs only termwise measurability and almost-everywhere summability; no integrability of the full random double sum is assumed in advance.

theorem Anderson4D.lintegral_operatorNormSq_le_of_weightedMomentBound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (A : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (bound : Z4 × Z4 → ℝ) (hbound_nonneg : ∀ (p : Z4 × Z4), 0 ≤ bound p) (hbound_sum : Summable bound) (hmeas : ∀ (p : Z4 × Z4), AEMeasurable (fun (ω : Ω) => ENNReal.ofReal (‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1)) μ) (hsum : ∀ᵐ (ω : Ω) ∂μ, Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) (hterm : ∀ (p : Z4 × Z4), ∫⁻ (ω : Ω), ENNReal.ofReal (‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) ∂μ ≤ ENNReal.ofReal (bound p)) : ∫⁻ (ω : Ω), ENNReal.ofReal (‖A ω‖ ^ 2) ∂μ ≤ ENNReal.ofReal (∑' (p : Z4 × Z4), bound p)

Numerical closure of the Tonelli estimate from termwise weighted second-moment bounds. This is the exact adapter between P-3.5b and P-L2: all probability is confined to hterm, while the remaining obligation is a deterministic summable majorant.

theorem Anderson4D.lintegral_ofReal_norm_sq_const_mul_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Ω → ℂ) (hf : MeasureTheory.MemLp f 2 μ) (c : ℂ) {w B : ℝ} (hw : 0 ≤ w) (hB : ∫ (ω : Ω), ‖f ω‖ ^ 2 ∂μ ≤ B) : ∫⁻ (ω : Ω), ENNReal.ofReal (‖c * f ω‖ ^ 2 * w) ∂μ ≤ ENNReal.ofReal (‖c‖ ^ 2 * B * w)

Turn an ordinary second-moment bound into the weighted lintegral bound consumed by lintegral_operatorNormSq_le_of_weightedMomentBound. The scalar c records normalization changes such as the paper-volume factor in the kernel/operator ledger.

The concrete orderwise P-3.5b to P-L2 bridge

def Anderson4D.ParametrixOrderL2CoeffRealization (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) : Prop

An order-m bounded random operator realizes the physical random kernel P_m when its Fourier matrix coefficients equal the paper coefficients almost surely, including the inverse torus-volume normalization forced by the use of probability Haar measure in TorusL2.

Almost-sure equality is essential here: the noise model specifies random variables only up to null sets, and P-3.5b yields simultaneous square summability only almost surely. Requiring the equality at every sample would add a non-probabilistic regularity hypothesis not present in the paper.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.parametrixOrderL2WeightedMomentRHS (outerConstant powerConstant lam ε : ℝ) (m : ℕ) (α β : Z4) : ℝ

Deterministic weighted moment majorant after translating the paper-normalized coefficient to the probability-Haar operator coefficient.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.parametrixOrderL2WeightedMomentRHS_nonneg {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) : 0 ≤ parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m α β

theorem Anderson4D.parametrixOrder_weightedCoeff_measurable_and_bound {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hreal : ParametrixOrderL2CoeffRealization M ρ lam ε m A) (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (hε : 0 < ε) (hεle : ε ≤ 1) : AEMeasurable (fun (ω : M.Ω) => ENNReal.ofReal (‖torusFourierMatrixCoeff (A ω) α β‖ ^ 2 * paperL2FourierWeight ε α β)) MeasureTheory.volume ∧ ∫⁻ (ω : M.Ω), ENNReal.ofReal (‖torusFourierMatrixCoeff (A ω) α β‖ ^ 2 * paperL2FourierWeight ε α β) ≤ ENNReal.ofReal (parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m α β)

P-3.5b gives both measurability and the weighted term estimate needed by the Tonelli form of (3.30), with every normalization factor visible.

theorem Anderson4D.lintegral_parametrixOrder_normSq_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hreal : ParametrixOrderL2CoeffRealization M ρ lam ε m A) (hfubini : ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hmajorant : Summable fun (p : Z4 × Z4) => parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m p.2 p.1) (hsum : ∀ᵐ (ω : M.Ω), Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) : ∫⁻ (ω : M.Ω), ENNReal.ofReal (‖A ω‖ ^ 2) ≤ ENNReal.ofReal (∑' (p : Z4 × Z4), parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m p.2 p.1)

Orderwise P-3.5b to P-L2 closure. After the deterministic weighted majorant is summable and the realized coefficient square-sum is non-junk almost surely, the expected L² → L² norm is bounded by the sum of the explicit (3.24) × (3.30) majorant.

theorem Anderson4D.integral_parametrixOrder_normSq_le {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} (A : M.Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (hreal : ParametrixOrderL2CoeffRealization M ρ lam ε m A) (hfubini : ∀ (α β : Z4), PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ∀ (α β : Z4), ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hε : 0 < ε) (hεle : ε ≤ 1) (hmajorant : Summable fun (p : Z4 × Z4) => parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m p.2 p.1) (hsum : ∀ᵐ (ω : M.Ω), Summable fun (p : Z4 × Z4) => ‖torusFourierMatrixCoeff (A ω) p.2 p.1‖ ^ 2 * paperL2FourierWeight ε p.2 p.1) (hintA : MeasureTheory.Integrable (fun (ω : M.Ω) => ‖A ω‖ ^ 2) MeasureTheory.volume) : ∫ (ω : M.Ω), ‖A ω‖ ^ 2 ≤ ∑' (p : Z4 × Z4), parametrixOrderL2WeightedMomentRHS outerConstant powerConstant lam ε m p.2 p.1

Real-valued expectation form of the preceding theorem.

theorem Anderson4D.integral_operatorNormSq_le_paperL2FourierWeight {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (A : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) {ε : ℝ} (hε : 0 < ε) (hεle : ε ≤ 1) (hinner : ∀ (ω : Ω) (β : Z4), Summable fun (α : Z4) => ‖torusFourierMatrixCoeff (A ω) α β‖ ^ 2 * paperL2FourierWeight ε α β) (houter : ∀ (ω : Ω), Summable fun (β : Z4) => ∑' (α : Z4), ‖torusFourierMatrixCoeff (A ω) α β‖ ^ 2 * paperL2FourierWeight ε α β) (hintA : MeasureTheory.Integrable (fun (ω : Ω) => ‖A ω‖ ^ 2) μ) (hintCoeff : MeasureTheory.Integrable (fun (ω : Ω) => ∑' (β : Z4) (α : Z4), ‖torusFourierMatrixCoeff (A ω) α β‖ ^ 2 * paperL2FourierWeight ε α β) μ) : ∫ (ω : Ω), ‖A ω‖ ^ 2 ∂μ ≤ ∫ (ω : Ω), ∑' (β : Z4) (α : Z4), ‖torusFourierMatrixCoeff (A ω) α β‖ ^ 2 * paperL2FourierWeight ε α β ∂μ

Expectation adapter for (3.30). Once both nonnegative sides are integrable, the pointwise Fourier double-sum bound passes directly to expectation.

def Anderson4D.paperScaleParametrixGoodEvent {Ω : Type u_1} (Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε : ℝ) : Set Ω

The precise norm thresholds used after (3.32). In the factorized bounded-operator realization, Q * greenL2Op is the paper parametrix.

Equations

• Anderson4D.paperScaleParametrixGoodEvent Q Rleft Rright ε = {ω : Ω | ‖Q ω‖ ≤ ε ^ (-14) ∧ ‖Rleft ω‖ + ‖Rright ω‖ ≤ ε ^ 28}

theorem Anderson4D.paperScaleParametrixGoodEvent_subset_twoSided {Ω : Type u_1} (Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε : ℝ) (hεpow : ε ^ 28 < 1 / 2) : paperScaleParametrixGoodEvent Q Rleft Rright ε ⊆ twoSidedParametrixGoodEvent Rleft Rright

The paper-scale remainder threshold implies the half-ball event used by the Banach-algebra inversion theorem.

theorem Anderson4D.lopInvertible_on_paperScaleParametrixGoodEvent {Ω : Type u_1} (M Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε : ℝ) (hdata : ∀ (ω : Ω), AndersonParametrixData greenL2Op (M ω) (Q ω) (Rleft ω) (Rright ω)) (hεpow : ε ^ 28 < 1 / 2) {ω : Ω} (hω : ω ∈ paperScaleParametrixGoodEvent Q Rleft Rright ε) : LopInvertible greenL2Op (M ω)

Membership in the paper-scale event constructs the factorized Anderson inverse.

theorem Anderson4D.norm_inverseGreen_sub_parametrix_on_paperScaleGoodEvent {Ω : Type u_1} (M Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε : ℝ) (hdata : ∀ (ω : Ω), AndersonParametrixData greenL2Op (M ω) (Q ω) (Rleft ω) (Rright ω)) (hεpos : 0 < ε) (hεsmall : 2 * ε ^ 2 ≤ 1) (hεpow : ε ^ 28 < 1 / 2) {ω : Ω} (hω : ω ∈ paperScaleParametrixGoodEvent Q Rleft Rright ε) : ‖inverseGreen greenL2Op (M ω) ⋯ - Q ω * greenL2Op‖ ≤ ε ^ 12

Quantitative form of (3.33) for the factorized bounded-operator realization.

theorem Anderson4D.norm_inverseGreen_sub_parametrix_on_paperScaleGoodEvent_of_half {Ω : Type u_1} (M Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε : ℝ) (hdata : ∀ (ω : Ω), AndersonParametrixData greenL2Op (M ω) (Q ω) (Rleft ω) (Rright ω)) (hεpos : 0 < ε) (hεle : ε ≤ 1 / 2) {ω : Ω} (hω : ω ∈ paperScaleParametrixGoodEvent Q Rleft Rright ε) : ‖inverseGreen greenL2Op (M ω) ⋯ - Q ω * greenL2Op‖ ≤ ε ^ 12

The elementary small-ε hypotheses needed by the preceding theorem follow from the convenient range 0 < ε ≤ 1/2.

First-moment control of the event

theorem Anderson4D.measureReal_norm_ge_le_div_firstMoment {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (F : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (r δ : ℝ) (hr : 0 < r) (hint : MeasureTheory.Integrable (fun (ω : Ω) => ‖F ω‖) μ) (hfirst : ∫ (ω : Ω), ‖F ω‖ ∂μ ≤ δ) : μ.real {ω : Ω | r ≤ ‖F ω‖} ≤ δ / r

A thresholded first moment bounds the real measure of the corresponding norm-bad event.

theorem Anderson4D.measureReal_compl_paperScaleParametrixGoodEvent_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε δQ δR : ℝ) (hεpos : 0 < ε) (hintQ : MeasureTheory.Integrable (fun (ω : Ω) => ‖Q ω‖) μ) (hintR : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rleft ω‖ + ‖Rright ω‖) μ) (hfirstQ : ∫ (ω : Ω), ‖Q ω‖ ∂μ ≤ δQ) (hfirstR : ∫ (ω : Ω), ‖Rleft ω‖ + ‖Rright ω‖ ∂μ ≤ δR) : μ.real (paperScaleParametrixGoodEvent Q Rleft Rright ε)ᶜ ≤ δQ / ε ^ (-14) + δR / ε ^ 28

Markov and the union bound control failure of the two paper-scale thresholds. The remainder sum is treated as one nonnegative random variable, exactly as in (3.32).

theorem Anderson4D.measureReal_compl_paperScaleParametrixGoodEvent_le_two_mul_sq {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (Q Rleft Rright : Ω → ↥TorusL2 →L[ℂ] ↥TorusL2) (ε : ℝ) (hεpos : 0 < ε) (hintQ : MeasureTheory.Integrable (fun (ω : Ω) => ‖Q ω‖) μ) (hintR : MeasureTheory.Integrable (fun (ω : Ω) => ‖Rleft ω‖ + ‖Rright ω‖) μ) (hfirstQ : ∫ (ω : Ω), ‖Q ω‖ ∂μ ≤ ε ^ (-12)) (hfirstR : ∫ (ω : Ω), ‖Rleft ω‖ + ‖Rright ω‖ ∂μ ≤ ε ^ 30) : μ.real (paperScaleParametrixGoodEvent Q Rleft Rright ε)ᶜ ≤ 2 * ε ^ 2

Substituting the two estimates in (3.32) gives the advertised O(ε²) exceptional-event probability, with the explicit union-bound constant 2.