Stat.Concentration.Variance­Adaptive­VCExpected­Maximal

theorem HasPolynomialL2Cover.hasPolynomialEmpiricalL2Cover {F : ι → 𝒳 → ℝ} {U : ℝ} (hF : HasPolynomialL2Cover F U) : ∃ A v : ℝ, exp 1 ≤ A ∧ 1 ≤ v ∧ HasPolynomialEmpiricalL2Cover F U A v := by /- Extract `A₀,p` from `hF.entropy` and take `A = max (exp 1) (2 * A₀)` and `v = (p + 1 : ℕ)`. Instantiate the arbitrary-measure certificate at `finiteSampleMeasure S`. For `x = A₀ / ε`, the hypotheses give `1 ≤ x`; hence `ceil (x^p) ≤ x^p + 1 ≤ 2*x^p ≤ (A/ε)^(p+1)`. Rewrite the final natural power as `rpow` with `Real.rpow_natCast`. -/ obtain ⟨A₀, p, hA₀, hentropy⟩ := hF.entropy refine ⟨max (exp 1) (2 * A₀), ((p + 1 : ℕ) : ℝ), le_max_left _ _, ?_, ?_⟩ · exact_mod_cast Nat.succ_le_succ (zero_le p) · intro m S hm ε hε hε1 letI : IsProbabilityMeasure (finiteSampleMeasure S) := finiteSampleMeasure_isProbabilityMeasure S hm obtain ⟨C, hCcard, hCcover⟩ := hentropy (finiteSampleMeasure S) inferInstance ε hε hε1 refine ⟨C, hCcover, ?_⟩ have hx : 1 ≤ A₀ / ε := (one_le_div hε).2 (hε1.trans hA₀) have hceil : (ceil ((A₀ / ε) ^ p) : ℝ) < (A₀ / ε) ^ p + 1 := Nat.ceil_lt_add_one (by positivity) have hxpow : 1 ≤ (A₀ / ε) ^ p := one_le_pow₀ hx have hbase : A₀ / ε ≤ max (exp 1) (2 * A₀) / ε := by apply div_le_div_of_nonneg_right _ hε.le exact (by linarith : A₀ ≤ 2 * A₀) |>.trans (le_max_right _ _) have htwo : 2 ≤ max (exp 1) (2 * A₀) / ε := by apply (le_div_iff₀ hε).2 calc 2 * ε ≤ 2 * 1 := by gcongr _ ≤ 2 * A₀ := by gcongr _ ≤ max (exp 1) (2 * A₀) := le_max_right _ _ calc (C.card : ℝ) ≤ (ceil ((A₀ / ε) ^ p) : ℝ) := by exact_mod_cast hCcard _ ≤ 2 * (A₀ / ε) ^ p := by linarith _ ≤ (max (exp 1) (2 * A₀) / ε) ^ (p + 1) := by have hp := pow_le_pow_left₀ (by positivity : 0 ≤ A₀ / ε) hbase p calc 2 * (A₀ / ε) ^ p ≤ (max (exp 1) (2 * A₀) / ε) * (A₀ / ε) ^ p := mul_le_mul_of_nonneg_right htwo (by positivity) _ ≤ (max (exp 1) (2 * A₀) / ε) * (max (exp 1) (2 * A₀) / ε) ^ p := mul_le_mul_of_nonneg_left hp (by positivity) _ = (max (exp 1) (2 * A₀) / ε) ^ (p + 1) := by rw [pow_succ] ring _ = rpow (max (exp 1) (2 * A₀) / ε) ((p + 1 : ℕ) : ℝ) := by exact (Real.rpow_natCast _ _).symm

theorem HasPolynomialEmpiricalL2Cover.coveringNumber_le {F : ι → 𝒳 → ℝ} {U A v : ℝ} (hcover : HasPolynomialEmpiricalL2Cover F U A v) (hmeas : ∀ i, Measurable (F i)) (hU : 0 < U) {n : ℕ} (S : Fin n → 𝒳) (hn : 0 < n) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) : let htot := hcover.totallyBounded hmeas hU S hn (coveringNumber htot (ε * U) : ℝ) ≤ rpow (A / ε) v := by /- Follow `real_vcSubgraph_empirical_coveringNumber_le`, using the explicit `hcover S hn ε hε hε1` witness instead of the pseudo-dimension cover. The minimal covering cardinality is at most the image of that witness, whose cardinality is bounded by the supplied real power. -/ classical dsimp only let htot := hcover.totallyBounded hmeas hU S hn let r := ε * U have hr : 0 < r := mul_pos hε hU obtain ⟨C, hCcover, hCcard⟩ := hcover S hn ε hε hε1 let T : Finset (EmpiricalFunctionSpace F S) := C.image fun j => ⟨j⟩ have hTcover : (Set.univ : Set (EmpiricalFunctionSpace F S)) ⊆ ⋃ y ∈ T, ball y r := by intro q hq obtain ⟨j, hjC, hj⟩ := hCcover q.index have hj' : empiricalDist S (F q.index) (F j) < r := by rw [← measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hn (hmeas q.index) (hmeas j)] exact hj refine Set.mem_iUnion_of_mem (⟨j⟩ : EmpiricalFunctionSpace F S) ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨j, hjC, rfl⟩) · exact hj' rw [coveringNumber_eq htot hr] calc (find (coveringNumber_exists htot hr) : ℝ) ≤ T.card := by exact_mod_cast Nat.find_min' (coveringNumber_exists htot hr) ⟨T, rfl, hTcover⟩ _ ≤ C.card := by exact_mod_cast Finset.card_image_le _ ≤ rpow (A / ε) v := hCcard

lemma vcEntropy_chaining_bound {Ω ι : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : ι → Ω → ℝ) (g0 : ℕ → ι) (U σ A v : ℝ) (hent : HasVCUniformEntropy μ g U σ A v) : ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n → ∫⁻ w, countableEmpiricalProcessSup μ g g0 w ∂Measure.pi (fun _ : Fin n => μ) ≤ ofReal (C * (σ * sqrt (log (U / σ) / n) + U * log (U / σ) / n)) := by rcases hent with ⟨hσ, hσU, hA, hv, hmeas, henv, hL2, hcover⟩ let L0 := log (U / σ) let L := vcMaximalLog A U σ let q := max (sqrt (v * L / L0)) (v * L / L0) let C := varianceAdaptiveVCConstant * q have hU : 0 < U := hσ.trans hσU have hratio : 1 < U / σ := (lt_div_iff₀ hσ).2 (by simpa using hσU) have hL0 : 0 < L0 := Real.log_pos hratio have hA1 : 1 ≤ A := (Real.one_le_exp (by norm_num)).trans hA have hbase : U / σ ≤ max (exp 1) (A * U / σ) := by apply le_trans ?_ (le_max_right _ _) calc U / σ ≤ A * (U / σ) := le_mul_of_one_le_left (div_nonneg hU.le hσ.le) hA1 _ = A * U / σ := by ring have hLle : L0 ≤ L := by dsimp only [L0, L, vcMaximalLog] exact Real.log_le_log (div_pos hU hσ) hbase have hL : 0 < L := hL0.trans_le hLle have hq : 0 < q := by dsimp only [q] exact lt_of_lt_of_le (div_pos (mul_pos (lt_of_lt_of_le zero_lt_one hv) hL) hL0) (le_max_right _ _) refine ⟨C, mul_pos (by norm_num [varianceAdaptiveVCConstant]) hq, ?_⟩ intro n hn have hn0 : 0 < n := Nat.zero_lt_of_lt hn let F : ℕ → Ω → ℝ := fun k => g (g0 k) let μn : Measure (Fin n → Ω) := Measure.pi (fun _ : Fin n => μ) have hFmeas : ∀ k, Measurable (F k) := fun k => hmeas (g0 k) have hFenv : ∀ k x, |F k x| ≤ U := fun k x => henv (g0 k) x have hmain := varianceAdaptiveExpectedMaximal_le μ F hσ hσU hA hv hFmeas hFenv (fun k => hL2 (g0 k)) (hcover g0) n hn0 have hrate := varianceAdaptiveRate_le_logRatio hσ hσU hA hv hn0 have hreal : ∫ w, countableEmpiricalSup μ F w ∂μn ≤ C * (σ * sqrt (log (U / σ) / (n : ℝ)) + U * log (U / σ) / (n : ℝ)) := by calc ∫ w, countableEmpiricalSup μ F w ∂μn ≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := hmain _ ≤ varianceAdaptiveVCConstant * (q * (σ * sqrt (log (U / σ) / (n : ℝ)) + U * log (U / σ) / (n : ℝ))) := mul_le_mul_of_nonneg_left hrate (by norm_num [varianceAdaptiveVCConstant]) _ = C * (σ * sqrt (log (U / σ) / (n : ℝ)) + U * log (U / σ) / (n : ℝ)) := by simp only [C]; ring have hdevMeas : Measurable (fun w : Fin n → Ω => countableEmpiricalSup μ F w) := by exact uniformDeviation_measurable id hFmeas have hdevBound : ∀ w : Fin n → Ω, countableEmpiricalSup μ F w ≤ 2 * U := by intro w exact countableEmpiricalSup_le_two_envelope μ g g0 hU hmeas henv hn0 w have hdevNonneg : ∀ w : Fin n → Ω, 0 ≤ countableEmpiricalSup μ F w := by intro w exact Real.iSup_nonneg fun k => abs_nonneg _ have hdevInt : Integrable (fun w : Fin n → Ω => countableEmpiricalSup μ F w) μn := Integrable.of_bound hdevMeas.aestronglyMeasurable (2 * U) (ae_of_all _ fun w => by rw [Real.norm_eq_abs, abs_of_nonneg (hdevNonneg w)] exact hdevBound w) simp_rw [countableEmpiricalProcessSup_eq_of_envelope μ g g0 hU hmeas henv hn0] rw [← ofReal_integral_eq_lintegral_ofReal hdevInt (ae_of_all _ hdevNonneg)] exact ENNReal.ofReal_le_ofReal hreal

theorem varianceAdaptiveExpectedMaximal_le [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {U σ A v : ℝ} (hσ : 0 < σ) (hσU : σ < U) (hA : exp 1 ≤ A) (hv : 1 ≤ v) (hmeas : ∀ i, Measurable (F i)) (henvelope : ∀ i x, |F i x| ≤ U) (hL2 : ∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ) (hcover : HasPolynomialEmpiricalL2Cover F U A v) (n : ℕ) (hn : 0 < n) : ∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P) ≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := by /- Apply countable-class symmetrization with the identity observation map, then substitute `varianceAdaptiveRademacherComplexity_le`. The envelope hypotheses make every indexed function integrable, and countability makes the pointwise supremum measurable; no continuum-supremum measurability premise is needed. -/ have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity (μ := P) (f := F) hn id (fun i => by simpa [Function.comp_def] using hmeas i) (hσ.trans hσU).le henvelope have hrad := varianceAdaptiveRademacherComplexity_le P F hσ hσU hA hv hmeas henvelope hL2 hcover n hn calc ∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P) ≤ 2 • rademacherComplexity n F P id := by simpa [countableEmpiricalSup, Function.comp_def] using hsymm _ ≤ 2 • ((varianceAdaptiveVCConstant / 2) * vcExpectedMaximalRate U σ A v n) := by have hmul := mul_le_mul_of_nonneg_left hrad (by norm_num : (0 : ℝ) ≤ 2) simp only [nsmul_eq_mul, Nat.cast_ofNat] exact hmul _ = varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := by simp only [nsmul_eq_mul] ring

theorem varianceAdaptiveRademacherComplexity_le [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {U σ A v : ℝ} (hσ : 0 < σ) (hσU : σ < U) (hA : exp 1 ≤ A) (hv : 1 ≤ v) (hmeas : ∀ i, Measurable (F i)) (henvelope : ∀ i x, |F i x| ≤ U) (hL2 : ∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ) (hcover : HasPolynomialEmpiricalL2Cover F U A v) (n : ℕ) (hn : 0 < n) : rademacherComplexity n F P id ≤ (varianceAdaptiveVCConstant / 2) * vcExpectedMaximalRate U σ A v n := by /- Proof route: 1. Anchor at one index and apply the existing signed Dudley theorem to the increment class (which contains zero). Bound the anchor directly by its empirical `L²` norm. This is the countable absolute-Dudley bridge; it avoids treating the signed theorem as if it already had an outer absolute value. 2. Conditional on a sample, use `hcover` and `measureL2Dist_finiteSampleMeasure_eq_empiricalDist` to bound every empirical covering number at envelope-relative scales. 3. Truncate Dudley's integral at a variable lower scale and at the random empirical radius `R_S = sup_f ‖f‖_{L²(Pₙ)}`. Integrate the polynomial entropy bound to obtain a conditional estimate proportional to `R_S * sqrt (v * log (max e (A*U/R_S)) / n)` plus the truncation term. 4. In the bounded-envelope specialization, symmetrization of the square class followed by `empiricalRademacherComplexity_contraction_abs_of_bddAbove` gives directly `E R_S² ≤ σ² + 8 U R_n(F)`; unlike the unbounded-envelope source proof, no Hoffmann–Jørgensen second-moment step is needed. Solve the resulting quadratic inequality, producing the leading `σ` term and the second-order `U/n` term. All constants may be rounded upward to `varianceAdaptiveVCConstant / 2`. -/ classical let μn : Measure (Fin n → 𝒳) := Measure.pi (fun _ : Fin n => P) have hU : 0 < U := hσ.trans hσU have hU0 : 0 ≤ U := hU.le have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast hn have hL1 : 1 ≤ vcMaximalLog A U σ := by have hratio : exp 1 < A * U / σ := by have hUσ : 1 < U / σ := (one_lt_div₀ hσ).2 hσU calc exp 1 ≤ A := hA _ < A * (U / σ) := by nlinarith [Real.exp_pos 1] _ = A * U / σ := by ring rw [vcMaximalLog, max_eq_right hratio.le, ← Real.log_exp 1] exact Real.log_le_log (Real.exp_pos 1) hratio.le have hv0 : 0 ≤ v := zero_le_one.trans hv have hvL1 : 1 ≤ v * vcMaximalLog A U σ := by nlinarith let rad : (Fin n → 𝒳) → ℝ := fun S => empiricalRademacherComplexity n F S let radius : (Fin n → 𝒳) → ℝ := fun S => empiricalL2Radius F S let floorRadius : ℝ := U / (n : ℝ) let radius' : (Fin n → 𝒳) → ℝ := fun S => max (radius S) floorRadius have hradMeas : Measurable rad := empiricalRademacherComplexity_measurable_countable F hmeas n have hradiusMeas : Measurable radius := empiricalL2Radius_measurable F hmeas n have hradius'Meas : Measurable radius' := hradiusMeas.max measurable_const have hradMem : ∀ S, rad S ∈ Icc 0 U := fun S => empiricalRademacherComplexity_mem_Icc F hU0 henvelope n S have hradiusMem : ∀ S, radius S ∈ Icc 0 U := fun S => empiricalL2Radius_mem_Icc F hU0 henvelope S have hfloor0 : 0 < floorRadius := div_pos hU hnR have hfloorU : floorRadius ≤ U := by dsimp [floorRadius] apply (div_le_iff₀ hnR).2 nlinarith have hradius'Mem : ∀ S, radius' S ∈ Icc 0 U := by intro S exact ⟨le_max_of_le_right hfloor0.le, max_le (hradiusMem S).2 hfloorU⟩ have hradInt : Integrable rad μn := (integrable_const U).mono' hradMeas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hradMem S).1] using (hradMem S).2) have hradiusInt : Integrable radius μn := (integrable_const U).mono' hradiusMeas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hradiusMem S).1] using (hradiusMem S).2) have hradius'Int : Integrable radius' μn := (integrable_const U).mono' hradius'Meas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hradius'Mem S).1] using (hradius'Mem S).2) let q : ℝ := sqrt (v * vcMaximalLog A U σ / (n : ℝ)) have hq0 : 0 ≤ q := Real.sqrt_nonneg _ have hconditional : ∀ S, rad S ≤ 26 * q * (radius' S + σ) := by intro S have hri : ∀ i, empiricalNorm S (F i) ≤ radius' S := by intro i have hbdd : BddAbove (range fun j => empiricalNorm S (F j)) := ⟨U, by rintro _ ⟨j, rfl⟩; exact empiricalNorm_le_of_envelope F hU0 henvelope S j⟩ exact (le_ciSup hbdd i).trans (le_max_left _ _) have hc := empiricalRademacher_conditional_le F hσ hσU hA hv hmeas henvelope hcover hn S hri (lt_of_lt_of_le hfloor0 (le_max_right _ _)) (hradius'Mem S).2 have hsqrt : sqrt (v * vcMaximalLog A U σ) / sqrt (n : ℝ) = q := by dsimp [q] rw [Real.sqrt_div (mul_nonneg hv0 (zero_le_one.trans hL1))] calc rad S ≤ 26 / sqrt (n : ℝ) * sqrt (v * vcMaximalLog A U σ) * (radius' S + σ) := hc _ = 26 * q * (radius' S + σ) := by rw [← hsqrt]; ring have hrhsInt : Integrable (fun S => 26 * q * (radius' S + σ)) μn := (hradius'Int.add (integrable_const σ)).const_mul _ have hxchain : rademacherComplexity n F P id ≤ 26 * q * ((∫ S, radius' S ∂μn) + σ) := by unfold rademacherComplexity change (∫ S, rad S ∂μn) ≤ _ calc (∫ S, rad S ∂μn) ≤ ∫ S, 26 * q * (radius' S + σ) ∂μn := integral_mono hradInt hrhsInt hconditional _ = 26 * q * ((∫ S, radius' S ∂μn) + σ) := by rw [integral_const_mul] rw [integral_add hradius'Int (integrable_const σ)] simp [μn, smul_eq_mul] have hradius'Expectation : (∫ S, radius' S ∂μn) ≤ (∫ S, radius S ∂μn) + floorRadius := by have hsumInt := hradiusInt.add (integrable_const floorRadius) calc (∫ S, radius' S ∂μn) ≤ ∫ S, radius S + floorRadius ∂μn := by apply integral_mono hradius'Int hsumInt intro S exact max_le_add_of_nonneg (hradiusMem S).1 hfloor0.le _ = (∫ S, radius S ∂μn) + floorRadius := by rw [integral_add hradiusInt (integrable_const floorRadius)] simp [μn] let sqF : ι → 𝒳 → ℝ := fun i x => F i x ^ 2 have hsqMeas : ∀ i, Measurable (sqF i) := fun i => (hmeas i).pow_const 2 have hsqEnv : ∀ i x, |sqF i x| ≤ U ^ 2 := by intro i x rw [abs_of_nonneg (sq_nonneg _), sq_le_sq] simpa [abs_of_pos hU] using henvelope i x have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity (μ := P) (f := sqF) hn id hsqMeas (sq_nonneg U) hsqEnv let φ : ℝ → ℝ := fun x => (clipIcc (-U) U x) ^ 2 have hφeq : ∀ i x, φ (F i x) = sqF i x := by intro i x simp [φ, sqF, clipIcc_neg_eq_self (henvelope i x)] have hφMeas : ∀ i, Measurable (fun x => φ (F i x)) := fun i => by simpa [hφeq i] using hsqMeas i have hcontractPoint : ∀ S, empiricalRademacherComplexity n sqF S ≤ 4 * U * rad S := by intro S have hc := empiricalRademacherComplexity_contraction_abs_of_bddAbove φ (clippedSquare_lipschitzAt0 hU0) F hU0 henvelope n S have heq := empiricalRademacherComplexity_congr_sample n sqF (fun i x => φ (F i x)) S (fun i k => (hφeq i (S k)).symm) rw [heq] calc empiricalRademacherComplexity n (fun i x => φ (F i x)) S ≤ 2 * (2 * U) * empiricalRademacherComplexity n F S := hc _ = 4 * U * rad S := by simp only [rad]; ring have hsqRadMeas := empiricalRademacherComplexity_measurable_countable sqF hsqMeas n have hsqRadInt : Integrable (fun S => empiricalRademacherComplexity n sqF S) μn := (integrable_const (U ^ 2)).mono' hsqRadMeas.aestronglyMeasurable (ae_of_all _ fun S => by have hm := empiricalRademacherComplexity_mem_Icc sqF (sq_nonneg U) hsqEnv n S simpa [Real.norm_eq_abs, abs_of_nonneg hm.1] using hm.2) have hcontractPop : rademacherComplexity n sqF P id ≤ 4 * U * rademacherComplexity n F P id := by unfold rademacherComplexity change (∫ S, empiricalRademacherComplexity n sqF S ∂μn) ≤ 4 * U * ∫ S, rad S ∂μn rw [← integral_const_mul] exact integral_mono hsqRadInt (hradInt.const_mul _) hcontractPoint have hdevExpectation : (∫ S, uniformDeviation n sqF P id S ∂μn) ≤ 8 * U * rademacherComplexity n F P id := by have hsymm' : (∫ S, uniformDeviation n sqF P id S ∂μn) ≤ 2 * rademacherComplexity n sqF P id := by simpa [μn, two_smul ℝ] using hsymm have hs := hsymm'.trans (mul_le_mul_of_nonneg_left hcontractPop (show (0 : ℝ) ≤ 2 by norm_num)) exact hs.trans_eq (by ring) have hradiusSqMeas : Measurable (fun S => radius S ^ 2) := hradiusMeas.pow_const 2 have hradiusSqInt : Integrable (fun S => radius S ^ 2) μn := (integrable_const (U ^ 2)).mono' hradiusSqMeas.aestronglyMeasurable (ae_of_all _ fun S => by rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] exact (sq_le_sq₀ (hradiusMem S).1 hU0).2 (hradiusMem S).2) have hdevMeas : Measurable (fun S => uniformDeviation n sqF P id S) := uniformDeviation_measurable id hsqMeas have hdevInt : Integrable (fun S => uniformDeviation n sqF P id S) μn := by have hsqInt : ∀ i, Integrable (sqF i) P := fun i => (integrable_const (U ^ 2)).mono' (hsqMeas i).aestronglyMeasurable (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hsqEnv i x) have hsqPop : ∀ i, (∫ x, sqF i x ∂P) ∈ Icc 0 (U ^ 2) := by intro i constructor · exact integral_nonneg fun x => by exact sq_nonneg (F i x) · calc (∫ x, sqF i x ∂P) ≤ ∫ _x, U ^ 2 ∂P := integral_mono (hsqInt i) (integrable_const (U ^ 2)) (fun x => by have := hsqEnv i x simpa [abs_of_nonneg (sq_nonneg (F i x)), sqF] using this) _ = U ^ 2 := by simp have hsqAvg : ∀ (T : Fin n → 𝒳) (i : ι), ((n : ℝ)⁻¹ * ∑ k : Fin n, sqF i (T k)) ∈ Icc 0 (U ^ 2) := by intro T i constructor · positivity · dsimp [sqF] calc _ ≤ (n : ℝ)⁻¹ * ∑ _k : Fin n, U ^ 2 := by refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun k _ => ?_) (by positivity) exact (sq_le_sq).2 (by simpa [abs_of_pos hU] using henvelope i (T k)) _ = U ^ 2 := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] simp only [Fintype.card_fin] field_simp have hdevBound : ∀ S, uniformDeviation n sqF P id S ∈ Icc 0 (2 * U ^ 2) := by intro S have hbdd : BddAbove (range fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, sqF i (S k) - ∫ x, sqF i x ∂P|) := by refine ⟨2 * U ^ 2, ?_⟩ rintro _ ⟨i, rfl⟩ have havg := hsqAvg S i have hpop := hsqPop i rw [abs_le] constructor <;> nlinarith [havg.1, havg.2, hpop.1, hpop.2, sq_nonneg U] constructor · let i₀ : ι := Classical.choice inferInstance unfold uniformDeviation exact (abs_nonneg _).trans (le_ciSup hbdd i₀) · unfold uniformDeviation exact ciSup_le fun i => by have havg := hsqAvg S i have hpop := hsqPop i simp only [Function.comp_apply, id_eq] rw [abs_le] constructor <;> nlinarith [havg.1, havg.2, hpop.1, hpop.2, sq_nonneg U] exact (integrable_const (2 * U ^ 2)).mono' hdevMeas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hdevBound S).1] using (hdevBound S).2) have hradiusSecond : (∫ S, radius S ^ 2 ∂μn) ≤ σ ^ 2 + 8 * U * rademacherComplexity n F P id := by have hpoint := fun S => empiricalL2Radius_sq_le_uniformDeviation P F hσ hσU hmeas henvelope hL2 hn S calc (∫ S, radius S ^ 2 ∂μn) ≤ ∫ S, σ ^ 2 + uniformDeviation n sqF P id S ∂μn := by -- … truncated; follow the source link for the rest …

-- @node: hasCountableEmpiricalSupReduction_of_pointwise_dense lemma hasCountableEmpiricalSupReduction_of_pointwise_dense {Ω ι : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [SigmaFinite μ] (g : ι → Ω → ℝ) (g0 : ℕ → ι) (S : Set Ω) (hS : ∀ᵐ z ∂μ, z ∈ S) (hdense : ∀ i, ∃ kseq : ℕ → ℕ, ∀ z ∈ S, Tendsto (fun m => g (g0 (kseq m)) z) atTop (nhds (g i z))) (hmeas : ∀ i, Measurable (g i)) (hdom : ∃ G : Ω → ℝ, Integrable G μ ∧ ∀ i z, |g i z| ≤ G z) : HasCountableEmpiricalSupReduction μ g := by rcases hdom with ⟨G, hG, hbound⟩ refine ⟨hmeas, g0, ?_⟩ intro n have hsampleS : ∀ᵐ w ∂Measure.pi (fun _ : Fin n => μ), ∀ j, w j ∈ S := eventually_all.2 fun j => Measure.tendsto_eval_ae_ae (μ := fun _ : Fin n => μ) (i := j) hS filter_upwards [hsampleS] with w hw apply le_antisymm · refine iSup_le fun i => ?_ obtain ⟨kseq, hseq⟩ := hdense i have hint : Tendsto (fun m => ∫ z, g (g0 (kseq m)) z ∂μ) atTop (nhds (∫ z, g i z ∂μ)) := by refine MeasureTheory.tendsto_integral_of_dominated_convergence G (fun m => (hmeas _).aestronglyMeasurable) hG ?_ ?_ · intro m exact Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hbound (g0 (kseq m)) z · exact hS.mono fun z hz => hseq z hz have havg : Tendsto (fun m => centeredEmpiricalAverage μ w (g (g0 (kseq m)))) atTop (nhds (centeredEmpiricalAverage μ w (g i))) := by unfold centeredEmpiricalAverage apply Tendsto.sub · apply Tendsto.const_mul apply tendsto_finset_sum intro j _hj exact hseq (w j) (hw j) · exact hint have hval : Tendsto (fun m => ofReal |centeredEmpiricalAverage μ w (g (g0 (kseq m)))|) atTop (nhds (ofReal |centeredEmpiricalAverage μ w (g i)|)) := ENNReal.continuous_ofReal.continuousAt.tendsto.comp (continuous_abs.continuousAt.tendsto.comp havg) apply le_of_tendsto hval exact Eventually.of_forall fun m => le_iSup (fun k : ℕ => ofReal |centeredEmpiricalAverage μ w (g (g0 k))|) (kseq m) · refine iSup_le fun k => ?_ exact le_iSup (fun i : ι => ofReal |centeredEmpiricalAverage μ w (g i)|) (g0 k)