Stat.EmpiricalProcess.Equicontinuity.LipschitzParametric
This module proves a measurable vector-valued maximal inequality for finite-dimensional Lipschitz score classes and derives stochastic equicontinuity for consistent estimators.
LipschitzParametric 6 core · 8 supporting This module proves a measurable vector-valued maximal inequality for finite-dimensional Lipschitz score classes and derives stochastic equicontinuity for consistent estimators. ★ parametricEmpProcSup_expected_le★ of_lipschitz★ of_lipschitz
Stochastic equicontinuity for Lipschitz parameter classes
This module proves a measurable vector-valued maximal inequality for finite-dimensional Lipschitz score classes and derives stochastic equicontinuity for consistent estimators.
def sampleEmpProc reviewed
⚑ flagged
Causalean.Stat
The centered root-sample-size empirical process compares the mean of a vector-valued function on a finite sample of size n with its mean under the population law.
def parametricEmpProcSup reviewed
⚑ flagged
Causalean.Stat
The measurable local empirical-process supremum takes the largest process norm along a canonical dense sequence in the ball with center and nonnegative radius. It evaluates the score family under the population law on a finite sample of size n.
Definition (Lean source)
parameters
def
parametricEmpProcSup P ψ θ₀ hδ n S :
ℝ
given by
⨆ k : ℕ, ‖sampleEmpProc P (fun x => ψ (closedBallDenseSeq θ₀ hδ k) x - ψ θ₀ x) n S‖
def lipschitzParametricConstant reviewed
⚑ flagged
Causalean.Stat
The dimension-only constant in the Lipschitz parametric maximal inequality is 192 times the dimension of the output space times one plus the dimension of the parameter space.
Definition (Lean source)
parameters
E V :
def
lipschitzParametricConstant E V :
ℝ
theorem parametricEmpProcSup_expected_le reviewed
⚑ flagged
Causalean.Stat
Quantitative finite-dimensional Lipschitz maximal inequality. For a population law, positive sample size, vector score, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, global Lipschitz control, center, and positive radius, the expected local empirical-process supremum is at most a dimension constant times the radius and envelope L² norm.
Formal statement
hypotheses
X E V :
P :
n :
ℕ
hn :
0 < n
ψ :
E → X → V
L :
X → ℝ
hψmeas :
∀ θ, Measurable (ψ θ)
hLmeas :
hL :
∀ x, 0 ≤ L x
hL2 :
Integrable (fun x => L x ^ 2) P
θ₀ :
E
δ :
ℝ
hLip :
∀ θ ∈ closedBall θ₀ δ,
∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖
hδ :
0 < δ
conclusion
≤ lipschitzParametricConstant E V * δ * sqrt (∫ x, L x ^ 2 ∂P)
Proof (Lean source)
theorem parametricEmpProcSup_expected_le
{X E V : Type*} [MeasurableSpace X]
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
[NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
[MeasurableSpace V] [BorelSpace V]
(P : Measure X) [IsProbabilityMeasure P]
{n : ℕ} (hn : 0 < n) (ψ : E → X → V) (L : X → ℝ)
(hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L)
(hL : ∀ x, 0 ≤ L x)
(hL2 : Integrable (fun x => L x ^ 2) P)
(θ₀ : E) {δ : ℝ}
(hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z,
‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖)
(hδ : 0 < δ) :
∫ S : Fin n → X, parametricEmpProcSup P ψ θ₀ hδ.le n S
∂Measure.pi (fun _ : Fin n => P) ≤
lipschitzParametricConstant E V * δ *
sqrt (∫ x, L x ^ 2 ∂P) :=
(parametricEmpProcSup_integrable_and_expected_le P hn ψ L hψmeas hLmeas hL hL2
θ₀ hLip hδ).2
theorem of_lipschitz reviewed
⚑ flagged
Causalean.Stat.AsymptoticEquicont
Lipschitz asymptotic equicontinuity (van der Vaart 1998, Example 19.7). For a population law, iid sample, vector score, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, target, a positive radius, and Lipschitz control on the ball of that radius, the score family is asymptotically equicontinuous at the target under the sampling measure.
Formal statement
hypotheses
Ω X E V :
P :
Measure X
S :
IIDSample Ω X μ P
ψ :
E → X → V
L :
X → ℝ
hψmeas :
∀ θ, Measurable (ψ θ)
hLmeas :
hL :
∀ x, 0 ≤ L x
hL2 :
Integrable (fun x => L x ^ 2) P
θ₀ :
E
δ₀ :
ℝ
hδ₀ :
0 < δ₀
hLip :
∀ θ ∈ closedBall θ₀ δ₀,
∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖
conclusion
AsymptoticEquicont ψ θ₀ P μ S
Proof (Lean source)
theorem of_lipschitz
{Ω X E V : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
[NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
[MeasurableSpace V] [BorelSpace V]
{μ : Measure Ω} (P : Measure X)
(S : IIDSample Ω X μ P) (ψ : E → X → V) (L : X → ℝ)
(hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L)
(hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P)
(θ₀ : E) {δ₀ : ℝ} (hδ₀ : 0 < δ₀)
(hLip : ∀ θ ∈ closedBall θ₀ δ₀, ∀ η ∈ closedBall θ₀ δ₀, ∀ z,
‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) :
AsymptoticEquicont ψ θ₀ P μ S := by
classical
haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
intro ε hε η hη
let M : ℝ := lipschitzParametricConstant E V *
sqrt (∫ x, L x ^ 2 ∂P)
have hmoment : 0 ≤ ∫ x, L x ^ 2 ∂P := integral_nonneg fun x => sq_nonneg (L x)
have hM : 0 ≤ M := by
dsimp [M, lipschitzParametricConstant]
positivity
let δ : ℝ := min (ε * η / (2 * (M + 1))) δ₀
have hδ : 0 < δ := by
dsimp [δ]
exact lt_min (by positivity) hδ₀
have hδsmall : δ ≤ ε * η / (2 * (M + 1)) := min_le_left _ _
have hδball : δ ≤ δ₀ := min_le_right _ _
-- Restrict the ball-Lipschitz hypothesis from radius `δ₀` inward to the chosen `δ`.
have hLipδ : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z,
‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖ := fun θ hθ η hη z =>
hLip θ (Metric.closedBall_subset_closedBall hδball hθ) η
(Metric.closedBall_subset_closedBall hδball hη) z
refine ⟨δ, hδ, ?_⟩
filter_upwards [eventually_gt_atTop (0 : ℕ)] with n hn
let Q : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => P)
let U : (Fin n → X) → ℝ :=
fun T => parametricEmpProcSup P ψ θ₀ hδ.le n T
have hUInt : Integrable U Q := by
simpa [U, Q] using parametricEmpProcSup_integrable P hn ψ L hψmeas hLmeas
hL hL2 θ₀ hLipδ hδ
have hUmeas : Measurable U := by
simpa [U] using parametricEmpProcSup_measurable P ψ θ₀ hδ.le n hψmeas
have hUnonneg : ∀ T, 0 ≤ U T := by
intro T
dsimp [U, parametricEmpProcSup]
exact Real.iSup_nonneg fun k => norm_nonneg _
have hUint : ∫ T, U T ∂Q ≤ M * δ := by
have hb :=
parametricEmpProcSup_expected_le P hn ψ L hψmeas hLmeas hL hL2 θ₀ hLipδ hδ
dsimp [U, Q, M]
calc
_ ≤ lipschitzParametricConstant E V * δ *
sqrt (∫ x, L x ^ 2 ∂P) := hb
_ = _ := by ring
have hratio : (∫ T, U T ∂Q) / ε ≤ η := by
calc
(∫ T, U T ∂Q) / ε ≤ (M * δ) / ε :=
div_le_div_of_nonneg_right hUint hε.le
_ ≤ (M * (ε * η / (2 * (M + 1)))) / ε := by gcongr
_ ≤ η := by
have hMone : 0 < M + 1 := by linarith
field_simp
nlinarith [mul_nonneg hM hη.le]
let A : Set (Fin n → X) := {T | ε < U T}
have hAmeas : MeasurableSet A := measurableSet_Ioi.preimage hUmeas
have hmarkov : Q A ≤ ofReal η := by
have hsub : A ⊆ {T | ofReal ε ≤ ofReal (U T)} := by
intro T hT
exact ENNReal.ofReal_le_ofReal hT.le
have hεne : ofReal ε ≠ 0 := ne_of_gt (ENNReal.ofReal_pos.mpr hε)
have hεtop : ofReal ε ≠ ⊤ := ENNReal.ofReal_ne_top
calc
Q A ≤ Q {T | ofReal ε ≤ ofReal (U T)} := measure_mono hsub
_ ≤ (∫⁻ T, ofReal (U T) ∂Q) / ofReal ε :=
MeasureTheory.meas_ge_le_lintegral_div hUmeas.ennreal_ofReal.aemeasurable
hεne hεtop
_ = ofReal (∫ T, U T ∂Q) / ofReal ε := by
rw [MeasureTheory.ofReal_integral_eq_lintegral_ofReal hUInt
(ae_of_all _ hUnonneg)]
_ = ofReal ((∫ T, U T ∂Q) / ε) := by
rw [ENNReal.ofReal_div_of_pos hε]
_ ≤ ofReal η := ENNReal.ofReal_le_ofReal hratio
let W : Ω → (Fin n → X) := fun ω k => S.Z k ω
have hWmeas : Measurable W := iidSample_finN_measurable S n
have htransport : μ (W ⁻¹' A) = Q A := by
rw [← Measure.map_apply hWmeas hAmeas, iidSample_finN_pushforward S n]
calc
μ {ω | ∃ θ : E, ‖θ - θ₀‖ < δ ∧
ε < ‖S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω‖}
≤ μ (W ⁻¹' A) := by
apply measure_mono
rintro ω ⟨θ, hθ, hproc⟩
have hle := sampleEmpProc_norm_le_parametricSup P ψ L hψmeas hLmeas hL hL2
θ₀ hLipδ hδ (W ω) θ hθ.le
have heq := sampleEmpProc_eq_empProcVec S
(fun z => ψ θ z - ψ θ₀ z) hn ω
exact hproc.trans_le (by simpa [W, U, A, heq] using hle)
_ = Q A := htransport
_ ≤ ofReal η := hmarkov
theorem of_lipschitz reviewed
⚑ flagged
Causalean.Stat.StochEquicontAt
Estimator-indexed Lipschitz equicontinuity (van der Vaart 1998, Lemma 19.24). For a population law, iid sample, vector score, nonnegative envelope, score and envelope measurability, envelope nonnegativity and square integrability, target, a positive radius, Lipschitz control on the ball of that radius, estimator sequence, and consistency, the estimator-indexed stochastic equicontinuity condition holds: for each positive threshold, some target neighborhood makes the sampling measure of a larger centered score increment there tend to zero.
Formal statement
hypotheses
Ω X E V :
P :
Measure X
S :
IIDSample Ω X μ P
ψ :
E → X → V
L :
X → ℝ
hψmeas :
∀ θ, Measurable (ψ θ)
hLmeas :
hL :
∀ x, 0 ≤ L x
hL2 :
Integrable (fun x => L x ^ 2) P
θ₀ :
E
δ₀ :
ℝ
hδ₀ :
0 < δ₀
hLip :
∀ θ ∈ closedBall θ₀ δ₀,
∀ η ∈ closedBall θ₀ δ₀, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖
θn :
ℕ → Ω → E
conclusion
StochEquicontAt ψ θ₀ P μ S θn
Proof (Lean source)
theorem of_lipschitz
{Ω X E V : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
[NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
[NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
[MeasurableSpace V] [BorelSpace V]
{μ : Measure Ω} (P : Measure X)
(S : IIDSample Ω X μ P) (ψ : E → X → V) (L : X → ℝ)
(hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L)
(hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P)
(θ₀ : E) {δ₀ : ℝ} (hδ₀ : 0 < δ₀)
(hLip : ∀ θ ∈ closedBall θ₀ δ₀, ∀ η ∈ closedBall θ₀ δ₀, ∀ z,
‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖)
(θn : ℕ → Ω → E)
(hConsistent : ∀ ε > 0,
Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) :
StochEquicontAt ψ θ₀ P μ S θn :=
stochEquicontAt_of_asymptoticEquicont ψ θ₀ S θn
(AsymptoticEquicont.of_lipschitz P S ψ L hψmeas hLmeas hL hL2 θ₀ hδ₀ hLip)
hConsistent
8 supporting declarations (lemmas, instances)
-
parametricEmpProcSup_measurabletheorem — The dense-sequence empirical-process supremum is measurable when every score is measurable. The supremum is formed from a score family, population law, center, nonnegative radius, and sample size.hypothesesconclusionProof (Lean source)
@[fun_prop] theorem parametricEmpProcSup_measurable {X E V : Type*} [MeasurableSpace X] [PseudoMetricSpace E] [SecondCountableTopology E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (P : Measure X) (ψ : E → X → V) (θ₀ : E) {δ : ℝ} (hδ : 0 ≤ δ) (n : ℕ) (hψmeas : ∀ θ, Measurable (ψ θ)) : Measurable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ n S) := by unfold parametricEmpProcSup apply Measurable.iSup intro k have hf : Measurable (fun x => ψ (closedBallDenseSeq θ₀ hδ k) x - ψ θ₀ x) := (hψmeas _).sub (hψmeas θ₀) have hp : Measurable (fun S : Fin n → X => sampleEmpProc P (fun x => ψ (closedBallDenseSeq θ₀ hδ k) x - ψ θ₀ x) n S) := by unfold sampleEmpProc fun_prop exact hp.norm -
uniformDeviation_integrable_of_envelopelemma — The uniform empirical deviation of a countable scalar class is integrable under a population probability law for positive sample size, provided the class and its envelope are respectively measurable and integrable, and the envelope dominates the class pointwise.hypothesesX ι :P :n :ℕhn :0 < nF :ι → X → ℝG :X → ℝhFmeas :∀ i, Measurable (F i)hGint :Integrable G Phenv :∀ i x, |F i x| ≤ G xconclusionProof (Lean source)
@[fun_prop] lemma uniformDeviation_integrable_of_envelope {X ι : Type*} [MeasurableSpace X] [Nonempty ι] [Countable ι] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (F : ι → X → ℝ) (G : X → ℝ) (hFmeas : ∀ i, Measurable (F i)) (hGint : Integrable G P) (henv : ∀ i x, |F i x| ≤ G x) : Integrable (fun S : Fin n → X => uniformDeviation n F P id S) (Measure.pi (fun _ : Fin n => P)) := by have hFint (i : ι) : Integrable (F i) P := Integrable.mono' hGint (hFmeas i).aestronglyMeasurable (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using henv i x) have hcoord (k : Fin n) : Integrable (fun S : Fin n → X => G (S k)) (Measure.pi (fun _ : Fin n => P)) := by change Integrable (G ∘ (fun S : Fin n → X => S k)) _ exact ((measurePreserving_eval (fun _ : Fin n => P) k).integrable_comp hGint.aestronglyMeasurable).2 hGint have hdomInt : Integrable (fun S : Fin n → X => (n : ℝ)⁻¹ * ∑ k : Fin n, G (S k) + ∫ x, G x ∂P) (Measure.pi (fun _ : Fin n => P)) := ((integrable_finsetSum univ fun k _ => hcoord k).const_mul _).add (integrable_const _) have hmeas : Measurable (fun S : Fin n → X => uniformDeviation n F P id S) := uniformDeviation_measurable id hFmeas apply Integrable.mono' hdomInt hmeas.aestronglyMeasurable filter_upwards with S rw [Real.norm_eq_abs, abs_of_nonneg (by unfold uniformDeviation exact Real.iSup_nonneg fun i => abs_nonneg _)] unfold uniformDeviation simp only [id_eq] apply ciSup_le intro i have havg : |(n : ℝ)⁻¹ * ∑ k : Fin n, F i (S k)| ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, G (S k) := by rw [abs_mul, abs_of_pos (inv_pos.mpr (by exact_mod_cast hn))] gcongr exact (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum fun k _ => henv i (S k)) have hint : |∫ x, F i x ∂P| ≤ ∫ x, G x ∂P := by calc _ ≤ ∫ x, |F i x| ∂P := abs_integral_le_integral_abs _ ≤ ∫ x, G x ∂P := integral_mono (hFint i).abs hGint (henv i) exact (abs_sub _ _).trans (add_le_add havg hint) -
norm_le_sum_abs_inner_basislemma — A finite-dimensional vector's norm is at most the sum of its absolute coordinates in the standard orthonormal basis, for the given vector.hypothesesV :v :VconclusionProof (Lean source)
lemma norm_le_sum_abs_inner_basis {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (v : V) : ‖v‖ ≤ ∑ j : Fin (finrank ℝ V), |inner ℝ ((stdOrthonormalBasis ℝ V) j) v| := by let b := stdOrthonormalBasis ℝ V calc ‖v‖ = ‖∑ j, (b.repr v).ofLp j • b j‖ := congrArg norm (b.sum_repr v).symm _ ≤ ∑ j, ‖(b.repr v).ofLp j • b j‖ := norm_sum_le _ _ _ = ∑ j, |inner ℝ (b j) v| := by apply Finset.sum_congr rfl intro j hj rw [norm_smul, Real.norm_eq_abs, b.repr_apply_apply, b.orthonormal.norm_eq_one, mul_one] -
parametricEmpProcSup_integrable_and_expected_letheorem — The measurable local empirical-process supremum is integrable and its expectation is bounded by the dimension constant times the radius and envelope norm. This holds under a population probability law at positive sample size for a measurable vector score with a measurable, nonnegative, square-integrable envelope, assuming Lipschitz control on the ball with center and positive radius.hypothesesX E V :P :n :ℕhn :0 < nψ :E → X → VL :X → ℝhψmeas :∀ θ, Measurable (ψ θ)hLmeas :hL :∀ x, 0 ≤ L xhL2 :Integrable (fun x => L x ^ 2) Pθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖hδ :0 < δconclusionconclusion 1Integrable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ.le n S) (Measure.pi (fun _ : Fin n => P))conclusion 2≤ lipschitzParametricConstant E V * δ * sqrt (∫ x, L x ^ 2 ∂P)Proof (Lean source)
theorem parametricEmpProcSup_integrable_and_expected_le {X E V : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (ψ : E → X → V) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hδ : 0 < δ) : Integrable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ.le n S) (Measure.pi (fun _ : Fin n => P)) ∧ ∫ S : Fin n → X, parametricEmpProcSup P ψ θ₀ hδ.le n S ∂Measure.pi (fun _ : Fin n => P) ≤ lipschitzParametricConstant E V * δ * sqrt (∫ x, L x ^ 2 ∂P) := by classical let b := stdOrthonormalBasis ℝ V let θseq := closedBallDenseSeq θ₀ hδ.le let Fv : ℕ → X → V := fun k x => ψ (θseq k) x - ψ θ₀ x let Fc : Fin (finrank ℝ V) → ℕ → X → ℝ := fun j k x => inner ℝ (b j) (Fv k x) have hLint : Integrable L P := by apply Integrable.mono' ((integrable_const (1 : ℝ)).add hL2) hLmeas.aestronglyMeasurable filter_upwards with x change |L x| ≤ 1 + L x ^ 2 rw [abs_of_nonneg (hL x)] nlinarith [sq_nonneg (L x - 1 / 2)] have hθ (k : ℕ) : ‖(θseq k).1 - θ₀‖ ≤ δ := by have hp := (θseq k).2 rw [Metric.mem_closedBall, dist_eq_norm] at hp exact hp have hFvmeas : ∀ k, Measurable (Fv k) := fun k => (hψmeas _).sub (hψmeas θ₀) have hFvenv : ∀ k x, ‖Fv k x‖ ≤ δ * L x := by intro k x calc ‖Fv k x‖ ≤ L x * ‖(θseq k).1 - θ₀‖ := by simpa [Fv] using hLip (θseq k).1 (θseq k).2 θ₀ (Metric.mem_closedBall_self hδ.le) x _ ≤ L x * δ := mul_le_mul_of_nonneg_left (hθ k) (hL x) _ = δ * L x := by ring have hFcmeas : ∀ j k, Measurable (Fc j k) := by intro j k fun_prop have hFcenv : ∀ j k x, |Fc j k x| ≤ δ * L x := by intro j k x calc |Fc j k x| ≤ ‖b j‖ * ‖Fv k x‖ := by simpa [Fc, Real.norm_eq_abs] using norm_inner_le_norm (𝕜 := ℝ) (b j) (Fv k x) _ = ‖Fv k x‖ := by rw [b.orthonormal.norm_eq_one, one_mul] _ ≤ δ * L x := hFvenv k x have hFcInt (j) : Integrable (fun S : Fin n → X => uniformDeviation n (Fc j) P id S) (Measure.pi (fun _ : Fin n => P)) := uniformDeviation_integrable_of_envelope P hn (Fc j) (fun x => δ * L x) (hFcmeas j) (hLint.const_mul δ) (hFcenv j) have hscalar (j : Fin (finrank ℝ V)) : ∫ S : Fin n → X, uniformDeviation n (Fc j) P id S ∂Measure.pi (fun _ : Fin n => P) ≤ 192 * (finrank ℝ E + 1) * δ * sqrt (∫ x, L x ^ 2 ∂P) / sqrt (n : ℝ) := by let Fj : E → X → ℝ := fun θ x => inner ℝ (b j) (ψ θ x - ψ θ₀ x) have hFjmeas : ∀ θ, Measurable (Fj θ) := by intro θ; fun_prop have hFjLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ x, |Fj θ x - Fj η x| ≤ L x * ‖θ - η‖ := by intro θ hθ η hη x calc |Fj θ x - Fj η x| = |inner ℝ (b j) (ψ θ x - ψ η x)| := by simp [Fj, inner_sub_right] _ ≤ ‖b j‖ * ‖ψ θ x - ψ η x‖ := by simpa [Real.norm_eq_abs] using norm_inner_le_norm (𝕜 := ℝ) (b j) (ψ θ x - ψ η x) _ = ‖ψ θ x - ψ η x‖ := by rw [b.orthonormal.norm_eq_one, one_mul] _ ≤ L x * ‖θ - η‖ := hLip θ hθ η hη x have hs := scalar_parametric_expected_average_le P hn Fj L hFjmeas hLmeas hL hL2 θ₀ hFjLip (by simp [Fj]) hδ change ∫ S : Fin n → X, uniformDeviation n ((fun θ : closedBall θ₀ δ => Fj θ.1) ∘ closedBallDenseSeq θ₀ hδ.le) P id S ∂Measure.pi (fun _ : Fin n => P) ≤ _ exact hs have hprocMeas (k : ℕ) : Measurable (fun S : Fin n → X => sampleEmpProc P (Fv k) n S) := by unfold sampleEmpProc fun_prop have hsupMeas : Measurable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ.le n S) := by unfold parametricEmpProcSup apply Measurable.iSup intro k fun_prop have hpoint (S : Fin n → X) : parametricEmpProcSup P ψ θ₀ hδ.le n S ≤ sqrt (n : ℝ) * ∑ j, uniformDeviation n (Fc j) P id S := by unfold parametricEmpProcSup apply ciSup_le intro k calc ‖sampleEmpProc P (Fv k) n S‖ ≤ ∑ j, |inner ℝ (b j) (sampleEmpProc P (Fv k) n S)| := norm_le_sum_abs_inner_basis _ _ ≤ ∑ j, sqrt (n : ℝ) * uniformDeviation n (Fc j) P id S := by apply Finset.sum_le_sum intro j hj have hFvint : Integrable (Fv k) P := Integrable.mono' (hLint.const_mul δ) (hFvmeas k).aestronglyMeasurable (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hFvenv k x) have hcoord : inner ℝ (b j) (sampleEmpProc P (Fv k) n S) = sqrt (n : ℝ) * ((n : ℝ)⁻¹ * ∑ i, Fc j k (S i) - ∫ x, Fc j k x ∂P) := by unfold sampleEmpProc simp only [inner_sub_right, real_inner_smul_right, inner_sum] rw [integral_inner hFvint (b j)] rw [hcoord, abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] gcongr unfold uniformDeviation exact le_ciSup (by refine ⟨δ * ((n : ℝ)⁻¹ * ∑ i, L (S i) + ∫ x, L x ∂P), ?_⟩ rintro _ ⟨q, rfl⟩ calc |(n : ℝ)⁻¹ * ∑ i, Fc j q (S i) - ∫ x, Fc j q x ∂P| ≤ (n : ℝ)⁻¹ * ∑ i, |Fc j q (S i)| + ∫ x, |Fc j q x| ∂P := by refine (abs_sub _ _).trans (add_le_add ?_ abs_integral_le_integral_abs) rw [abs_mul, abs_of_pos (inv_pos.mpr (by exact_mod_cast hn))] gcongr exact Finset.abs_sum_le_sum_abs _ _ _ ≤ δ * ((n : ℝ)⁻¹ * ∑ i, L (S i) + ∫ x, L x ∂P) := by have hFcqInt : Integrable (Fc j q) P := Integrable.mono' (hLint.const_mul δ) (hFcmeas j q).aestronglyMeasurable (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hFcenv j q x) have hi := integral_mono hFcqInt.abs (hLint.const_mul δ) (fun x => hFcenv j q x) rw [integral_const_mul] at hi calc _ ≤ (n : ℝ)⁻¹ * ∑ i, δ * L (S i) + δ * ∫ x, L x ∂P := by gcongr with i exact hFcenv j q (S i) _ = _ := by rw [← Finset.mul_sum]; ring) k _ = sqrt (n : ℝ) * ∑ j, uniformDeviation n (Fc j) P id S := by rw [Finset.mul_sum] have hdomInt : Integrable (fun S : Fin n → X => sqrt (n : ℝ) * ∑ j, uniformDeviation n (Fc j) P id S) (Measure.pi (fun _ : Fin n => P)) := (integrable_finsetSum univ fun j _ => hFcInt j).const_mul _ have hsupInt : Integrable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ.le n S) (Measure.pi (fun _ : Fin n => P)) := by apply Integrable.mono' hdomInt hsupMeas.aestronglyMeasurable filter_upwards with S rw [Real.norm_eq_abs, abs_of_nonneg (by unfold parametricEmpProcSup exact Real.iSup_nonneg fun k => norm_nonneg _)] exact hpoint S refine ⟨hsupInt, ?_⟩ calc _ ≤ ∫ S : Fin n → X, sqrt (n : ℝ) * ∑ j, uniformDeviation n (Fc j) P id S ∂Measure.pi (fun _ : Fin n => P) := integral_mono hsupInt hdomInt hpoint _ = sqrt (n : ℝ) * ∑ j, ∫ S : Fin n → X, uniformDeviation n (Fc j) P id S ∂Measure.pi (fun _ : Fin n => P) := by rw [integral_const_mul, integral_finsetSum univ (fun j _ => hFcInt j)] _ ≤ sqrt (n : ℝ) * ∑ _j : Fin (finrank ℝ V), (192 * (finrank ℝ E + 1) * δ * sqrt (∫ x, L x ^ 2 ∂P) / sqrt (n : ℝ)) := by gcongr with j exact hscalar j _ = lipschitzParametricConstant E V * δ * sqrt (∫ x, L x ^ 2 ∂P) := by simp [lipschitzParametricConstant] have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 (by exact_mod_cast hn) field_simp -
parametricEmpProcSup_integrabletheorem — The dense local empirical-process supremum is integrable under a population probability law at positive sample size for a measurable vector score with a measurable, nonnegative, square-integrable envelope, assuming Lipschitz control on the ball with center and positive radius.hypothesesX E V :P :n :ℕhn :0 < nψ :E → X → VL :X → ℝhψmeas :∀ θ, Measurable (ψ θ)hLmeas :hL :∀ x, 0 ≤ L xhL2 :Integrable (fun x => L x ^ 2) Pθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖hδ :0 < δconclusionIntegrable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ.le n S) (Measure.pi (fun _ : Fin n => P))Proof (Lean source)
@[fun_prop] theorem parametricEmpProcSup_integrable {X E V : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (ψ : E → X → V) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hδ : 0 < δ) : Integrable (fun S : Fin n → X => parametricEmpProcSup P ψ θ₀ hδ.le n S) (Measure.pi (fun _ : Fin n => P)) := (parametricEmpProcSup_integrable_and_expected_le P hn ψ L hψmeas hLmeas hL hL2 θ₀ hLip hδ).1 -
sampleEmpProc_eq_empProcVeclemma — The finite-product empirical process equals the sample-indexed empirical process vector for a vector-valued function evaluated on an i.i.d. sample at an outcome, provided the sample size is positive.hypothesesconclusionsampleEmpProc P f n (fun k : Fin n => S.Z k ω) = S.empProcVec f n ωProof (Lean source)
lemma sampleEmpProc_eq_empProcVec {Ω X V : Type*} [MeasurableSpace Ω] [MeasurableSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : Measure Ω} {P : Measure X} (S : IIDSample Ω X μ P) (f : X → V) {n : ℕ} (hn : 0 < n) (ω : Ω) : sampleEmpProc P f n (fun k : Fin n => S.Z k ω) = S.empProcVec f n ω := by unfold sampleEmpProc IIDSample.empProcVec change sqrt (n : ℝ) • ((n : ℝ)⁻¹ • (∑ i : Fin n, f (S.Z (i : ℕ) ω)) - ∫ x, f x ∂P) = _ rw [← Fin.sum_univ_eq_sum_range] have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 (by exact_mod_cast hn) have hsq : sqrt (n : ℝ) * sqrt (n : ℝ) = (n : ℝ) := Real.mul_self_sqrt (by positivity) have hcoef : sqrt (n : ℝ) * (n : ℝ)⁻¹ = (sqrt (n : ℝ))⁻¹ := by apply eq_inv_of_mul_eq_one_left calc (sqrt (n : ℝ) * (n : ℝ)⁻¹) * sqrt (n : ℝ) = (n : ℝ)⁻¹ * (sqrt (n : ℝ) * sqrt (n : ℝ)) := by ring _ = (n : ℝ)⁻¹ * (n : ℝ) := by rw [hsq] _ = 1 := inv_mul_cancel₀ (by exact_mod_cast hn.ne') rw [smul_sub, smul_smul, hcoef] -
sampleEmpProc_norm_le_parametricSuplemma — The empirical-process norm at a parameter in the ball is bounded by the measurable dense supremum. The bound applies under a population probability law to a measurable vector score with a measurable, nonnegative, square-integrable envelope and Lipschitz control, on the ball with center and positive radius, for sample and parameter in that ball.hypothesesX E V :P :ψ :E → X → VL :X → ℝhψmeas :∀ θ, Measurable (ψ θ)hLmeas :hL :∀ x, 0 ≤ L xhL2 :Integrable (fun x => L x ^ 2) Pθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖hδ :0 < δn :ℕS :Fin n → Xθ :Ehθ :‖θ - θ₀‖ ≤ δconclusion‖sampleEmpProc P (fun x => ψ θ x - ψ θ₀ x) n S‖ ≤ parametricEmpProcSup P ψ θ₀ hδ.le n SProof (Lean source)
lemma sampleEmpProc_norm_le_parametricSup {X E V : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (P : Measure X) [IsProbabilityMeasure P] (ψ : E → X → V) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ Metric.closedBall θ₀ δ, ∀ η ∈ Metric.closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hδ : 0 < δ) {n : ℕ} (S : Fin n → X) (θ : E) (hθ : ‖θ - θ₀‖ ≤ δ) : ‖sampleEmpProc P (fun x => ψ θ x - ψ θ₀ x) n S‖ ≤ parametricEmpProcSup P ψ θ₀ hδ.le n S := by classical let B := Metric.closedBall θ₀ δ let θsub : B := ⟨θ, by change θ ∈ Metric.closedBall θ₀ δ rw [Metric.mem_closedBall, dist_eq_norm] exact hθ⟩ letI : Nonempty B := ⟨⟨θ₀, by change dist θ₀ θ₀ ≤ δ simpa using hδ.le⟩⟩ letI : CompactSpace B := isCompact_iff_compactSpace.mp (by simpa [B] using (isCompact_closedBall θ₀ δ)) have hLint : Integrable L P := by apply Integrable.mono' ((integrable_const (1 : ℝ)).add hL2) hLmeas.aestronglyMeasurable filter_upwards with x change |L x| ≤ 1 + L x ^ 2 rw [abs_of_nonneg (hL x)] nlinarith [sq_nonneg (L x - 1 / 2)] let F : B → X → V := fun q x => ψ q.1 x - ψ θ₀ x have hFmeas (q : B) : Measurable (F q) := (hψmeas q.1).sub (hψmeas θ₀) have hFint (q : B) : Integrable (F q) P := by apply Integrable.mono' (hLint.const_mul ‖q.1 - θ₀‖) (hFmeas q).aestronglyMeasurable filter_upwards with x simpa [F, mul_comm] using hLip q.1 q.2 θ₀ (Metric.mem_closedBall_self hδ.le) x have hpointCont (x : X) : Continuous (fun q : B => F q x) := by let K : NNReal := ⟨L x, hL x⟩ apply (LipschitzWith.of_dist_le_mul (K := K) fun q r => ?_).continuous change dist (F q x) (F r x) ≤ L x * dist (q.1 : E) r.1 have hp := hLip q.1 q.2 r.1 r.2 x simpa [F, dist_eq_norm] using hp have hIntLip (q r : B) : dist (∫ x, F q x ∂P) (∫ x, F r x ∂P) ≤ (∫ x, L x ∂P) * dist q r := by have hDint : Integrable (fun x => F q x - F r x) P := (hFint q).sub (hFint r) rw [dist_eq_norm, ← integral_sub (hFint q) (hFint r)] calc ‖∫ x, F q x - F r x ∂P‖ ≤ ∫ x, ‖F q x - F r x‖ ∂P := norm_integral_le_integral_norm _ _ ≤ ∫ x, L x * dist q r ∂P := by apply integral_mono hDint.norm (hLint.mul_const _) intro x have hp := hLip q.1 q.2 r.1 r.2 x have hd : dist q r = ‖q.1 - r.1‖ := by change dist (q.1 : E) r.1 = _ rw [dist_eq_norm] rw [hd] simpa [F] using hp _ = (∫ x, L x ∂P) * dist q r := by rw [integral_mul_const] have hLintNonneg : 0 ≤ ∫ x, L x ∂P := integral_nonneg hL have hIntCont : Continuous (fun q : B => ∫ x, F q x ∂P) := by let K : NNReal := ⟨∫ x, L x ∂P, hLintNonneg⟩ exact (LipschitzWith.of_dist_le_mul (K := K) hIntLip).continuous have hprocCont : Continuous (fun q : B => sampleEmpProc P (F q) n S) := by unfold sampleEmpProc fun_prop have hnormCont : Continuous (fun q : B => ‖sampleEmpProc P (F q) n S‖) := continuous_norm.comp hprocCont have hbdd : BddAbove (Set.range fun q : B => ‖sampleEmpProc P (F q) n S‖) := (isCompact_range hnormCont).bddAbove have hsupEq := separableSpaceSup_eq_real hnormCont have hseq : closedBallDenseSeq θ₀ hδ.le = denseSeq B := by rfl calc ‖sampleEmpProc P (fun x => ψ θ x - ψ θ₀ x) n S‖ = ‖sampleEmpProc P (F θsub) n S‖ := rfl _ ≤ ⨆ q : B, ‖sampleEmpProc P (F q) n S‖ := le_ciSup hbdd θsub _ = ⨆ k : ℕ, ‖sampleEmpProc P (F (denseSeq B k)) n S‖ := hsupEq _ = parametricEmpProcSup P ψ θ₀ hδ.le n S := by unfold parametricEmpProcSup rw [hseq] -
parametricEmpProcSup_eq_iSup_closedBalltheorem — The measurable dense supremum equals the supremum over the entire closed parameter ball. Continuity follows under a population probability law from a measurable vector score with a measurable, nonnegative, square-integrable envelope and Lipschitz control, on the ball with center and positive radius, for the finite sample.hypothesesX E V :P :ψ :E → X → VL :X → ℝhψmeas :∀ θ, Measurable (ψ θ)hLmeas :hL :∀ x, 0 ≤ L xhL2 :Integrable (fun x => L x ^ 2) Pθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖hδ :0 < δn :ℕS :Fin n → XconclusionparametricEmpProcSup P ψ θ₀ hδ.le n S= ⨆ θ : closedBall θ₀ δ, ‖sampleEmpProc P (fun x => ψ θ.1 x - ψ θ₀ x) n S‖Proof (Lean source)
theorem parametricEmpProcSup_eq_iSup_closedBall {X E V : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (P : Measure X) [IsProbabilityMeasure P] (ψ : E → X → V) (L : X → ℝ) (hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖) (hδ : 0 < δ) {n : ℕ} (S : Fin n → X) : parametricEmpProcSup P ψ θ₀ hδ.le n S = ⨆ θ : closedBall θ₀ δ, ‖sampleEmpProc P (fun x => ψ θ.1 x - ψ θ₀ x) n S‖ := by let U : ℝ := parametricEmpProcSup P ψ θ₀ hδ.le n S have hfull (θ : closedBall θ₀ δ) : ‖sampleEmpProc P (fun x => ψ θ.1 x - ψ θ₀ x) n S‖ ≤ U := by apply sampleEmpProc_norm_le_parametricSup P ψ L hψmeas hLmeas hL hL2 θ₀ hLip hδ S θ.1 have hp := θ.2 rw [Metric.mem_closedBall, dist_eq_norm] at hp exact hp have hbdd : BddAbove (Set.range fun θ : closedBall θ₀ δ => ‖sampleEmpProc P (fun x => ψ θ.1 x - ψ θ₀ x) n S‖) := ⟨U, by rintro _ ⟨θ, rfl⟩; exact hfull θ⟩ letI : Nonempty (closedBall θ₀ δ) := ⟨⟨θ₀, by simp [hδ.le]⟩⟩ apply le_antisymm · unfold parametricEmpProcSup apply ciSup_le intro k exact le_ciSup hbdd (closedBallDenseSeq θ₀ hδ.le k) · apply ciSup_le exact hfull
Entropy 2 core · 5 supporting This module compares empirical score metrics with Euclidean parameter distance and derives the resulting finite-dimensional covering-number and Dudley-entropy bounds. ★ parametric_entropyIntegral_le
Entropy bounds for finite-dimensional Lipschitz parameter classes
This module compares empirical score metrics with Euclidean parameter distance and derives the resulting finite-dimensional covering-number and Dudley-entropy bounds.
def closedBallDenseSeq reviewed
⚑ flagged
Causalean.Stat
The chosen countable dense sequence in a closed ball is obtained from the ambient separability sequence for the ball with center and nonnegative radius.
Definition (Lean source)
parameters
def
given by
by letI : Nonempty (closedBall θ₀ δ) := ⟨⟨θ₀, by simpa [Metric.mem_closedBall] using hδ⟩⟩ exact denseSeq (closedBall θ₀ δ)
lemma parametric_entropyIntegral_le reviewed
⚑ flagged
Causalean.Stat
The truncated Dudley entropy integral of a Lipschitz class is bounded by dimension times radius on a sample. The scalar class has a nonnegative envelope and Lipschitz control on the ball with center and positive radius; the estimate assumes positive empirical envelope norm, positive cutoff, and a cutoff below the class radius.
Formal statement
hypotheses
X E :
n :
ℕ
S :
Fin n → X
F :
E → X → ℝ
L :
X → ℝ
hL :
∀ x, 0 ≤ L x
θ₀ :
E
δ :
ℝ
hLip :
∀ θ ∈ closedBall θ₀ δ,
∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖
hδ :
0 < δ
ha :
0 < Concentration.empiricalNorm S L
ε :
ℝ
hε :
0 < ε
hεR :
ε ≤ δ * Concentration.empiricalNorm S L
conclusion
ι :
closedBall θ₀ δ
htot :
parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ.le
Proof (Lean source)
lemma parametric_entropyIntegral_le
{X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{n : ℕ} (S : Fin n → X) (F : E → X → ℝ) (L : X → ℝ)
(hL : ∀ x, 0 ≤ L x)
(θ₀ : E) {δ : ℝ}
(hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z,
|F θ z - F η z| ≤ L z * ‖θ - η‖)
(hδ : 0 < δ)
(ha : 0 < Concentration.empiricalNorm S L)
{ε : ℝ} (hε : 0 < ε)
(hεR : ε ≤ δ * Concentration.empiricalNorm S L) :
let ι := closedBall θ₀ δ
let htot := parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ.le
(∫ x in ε..(δ * Concentration.empiricalNorm S L),
sqrt (log (Concentration.coveringNumber' htot x))) ≤
4 * (finrank ℝ E + 1) *
(δ * Concentration.empiricalNorm S L) := by
dsimp only
let R := δ * Concentration.empiricalNorm S L
let d : ℝ := finrank ℝ E
let htot := parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ.le
have hR : 0 < R := mul_pos hδ ha
have hd : 0 ≤ d := by positivity
have hlog9 : 0 ≤ log 9 := Real.log_nonneg (by norm_num)
letI : Nonempty (Concentration.EmpiricalFunctionSpace
(fun θ : closedBall θ₀ δ => F θ.1) S) :=
⟨⟨⟨θ₀, by simp [hδ.le]⟩⟩⟩
have hpoint : ∀ x ∈ Icc ε R,
sqrt (log (Concentration.coveringNumber' htot x)) ≤
sqrt (d * log 9) +
sqrt d * sqrt (log (R / x)) := by
intro x hx
have hx0 : 0 < x := hε.trans_le hx.1
have hxR : 1 ≤ R / x := (one_le_div hx0).2 hx.2
have hbase : 0 < 9 * R / x := by positivity
have hcov0 : 0 < (Concentration.coveringNumber' htot x : ℝ) := by
exact_mod_cast Concentration.coveringNumber'_nonzero Set.univ_nonempty htot hx0
have hcov := parametric_coveringNumber_le S F L hL θ₀ hLip hδ.le hx0
have hbase_le :
1 + 8 * δ * Concentration.empiricalNorm S L / x ≤ 9 * R / x := by
dsimp [R]
have hRx : x ≤ δ * Concentration.empiricalNorm S L := hx.2
calc
1 + 8 * δ * Concentration.empiricalNorm S L / x
≤ δ * Concentration.empiricalNorm S L / x +
8 * δ * Concentration.empiricalNorm S L / x := by
gcongr
_ = 9 * (δ * Concentration.empiricalNorm S L) / x := by ring
have hcov' : (Concentration.coveringNumber' htot x : ℝ) ≤
(9 * R / x) ^ finrank ℝ E := by
exact hcov.trans (pow_le_pow_left₀ (by positivity) hbase_le _)
have hlogcov : log (Concentration.coveringNumber' htot x) ≤
d * log (9 * R / x) := by
calc
log (Concentration.coveringNumber' htot x)
≤ log ((9 * R / x) ^ finrank ℝ E) :=
Real.log_le_log hcov0 hcov'
_ = d * log (9 * R / x) := by
rw [Real.log_pow]
have hsplit : log (9 * R / x) = log 9 + log (R / x) := by
rw [show 9 * R / x = 9 * (R / x) by ring]
exact Real.log_mul (by norm_num) (by positivity)
have hlogRx : 0 ≤ log (R / x) := Real.log_nonneg hxR
have hmain := Real.sqrt_le_sqrt hlogcov
have hsqrtadd : sqrt (d * log 9 + d * log (R / x)) ≤
sqrt (d * log 9) + sqrt (d * log (R / x)) := by
have ha' : 0 ≤ d * log 9 := mul_nonneg hd hlog9
have hb' : 0 ≤ d * log (R / x) := mul_nonneg hd hlogRx
nlinarith [Real.sq_sqrt ha', Real.sq_sqrt hb',
Real.sq_sqrt (add_nonneg ha' hb'),
Real.sqrt_nonneg (d * log 9),
Real.sqrt_nonneg (d * log (R / x))]
calc
sqrt (log (Concentration.coveringNumber' htot x))
≤ sqrt (d * log (9 * R / x)) := hmain
_ = sqrt (d * log 9 + d * log (R / x)) := by
rw [hsplit]
ring_nf
_ ≤ sqrt (d * log 9) + sqrt (d * log (R / x)) := hsqrtadd
_ = sqrt (d * log 9) +
sqrt d * sqrt (log (R / x)) := by
rw [Real.sqrt_mul hd, Real.sqrt_mul hd]
have hintLeft : IntervalIntegrable
(fun x : ℝ => sqrt (log (Concentration.coveringNumber' htot x)))
volume ε R := by
apply AntitoneOn.intervalIntegrable
refine antitoneOn_iff_forall_lt.mpr ?_
intro a haI b hbI hab
apply Real.sqrt_le_sqrt
apply Real.log_le_log
· exact_mod_cast Concentration.coveringNumber'_nonzero Set.univ_nonempty htot (by
have hb' : b ∈ Icc ε R := by
rw [← Set.uIcc_of_le hεR]
exact hbI
exact hε.trans_le hb'.1)
· norm_cast
exact Concentration.coveringNumber'_antitone htot
(by have ha' : a ∈ Icc ε R := by
rw [← Set.uIcc_of_le hεR]
exact haI
exact hε.trans_le ha'.1)
(by have hb' : b ∈ Icc ε R := by
rw [← Set.uIcc_of_le hεR]
exact hbI
exact hε.trans_le hb'.1) hab.le
have hintConst : IntervalIntegrable
(fun _x : ℝ => sqrt (d * log 9)) volume ε R :=
intervalIntegrable_const
have hintKernel : IntervalIntegrable
(fun x : ℝ => sqrt d * sqrt (log (R / x))) volume ε R :=
(Concentration.intervalIntegrable_sqrt_log_div hε hεR).const_mul _
have hmono := intervalIntegral.integral_mono_on hεR hintLeft
(hintConst.add hintKernel) hpoint
have hkernel := Concentration.sqrtLog_integral_le hε hεR
have hlog9le : log 9 ≤ 8 := by
exact (Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 9)).trans_eq (by norm_num)
have hsqrtdlog : sqrt (d * log 9) ≤ d + 3 := by
rw [Real.sqrt_le_iff]
constructor
· linarith
· have hmul : d * log 9 ≤ 8 * d := by
simpa [mul_comm] using mul_le_mul_of_nonneg_left hlog9le hd
nlinarith [sq_nonneg d]
have hsqrtd : sqrt d ≤ d + 1 := by
rw [Real.sqrt_le_iff]
constructor <;> nlinarith [sq_nonneg d]
calc
(∫ x in ε..R,
sqrt (log (Concentration.coveringNumber' htot x)))
≤ ∫ x in ε..R, (sqrt (d * log 9) +
sqrt d * sqrt (log (R / x))) := hmono
_ = (R - ε) * sqrt (d * log 9) +
sqrt d * (∫ x in ε..R, sqrt (log (R / x))) := by
rw [intervalIntegral.integral_add hintConst hintKernel]
rw [intervalIntegral.integral_const, intervalIntegral.integral_const_mul]
simp [smul_eq_mul]
_ ≤ R * sqrt (d * log 9) + sqrt d * R := by
have h1 : (R - ε) * sqrt (d * log 9) ≤
R * sqrt (d * log 9) := by
nlinarith [Real.sqrt_nonneg (d * log 9)]
have hkernelR : (∫ x in ε..R, sqrt (log (R / x))) ≤ R :=
hkernel.trans (by linarith)
have h2 := mul_le_mul_of_nonneg_left hkernelR (Real.sqrt_nonneg d)
nlinarith
_ ≤ 4 * (d + 1) * R := by nlinarith [hR.le]
_ = 4 * (finrank ℝ E + 1) *
(δ * Concentration.empiricalNorm S L) := rfl
5 supporting declarations (lemmas, instances)
-
empiricalNorm_le_mullemma — The empirical norm of a scalar function is at most the scaled empirical envelope norm on a finite sample, whenever the function is pointwise dominated by a nonnegative envelope times a nonnegative scale.hypothesesX :Type*n :ℕS :Fin n → Xf L :X → ℝa :ℝha :0 ≤ ahL :∀ x, 0 ≤ L xhf :∀ x, |f x| ≤ a * L xconclusionConcentration.empiricalNorm S f ≤ a * Concentration.empiricalNorm S LProof (Lean source)
lemma empiricalNorm_le_mul {X : Type*} {n : ℕ} (S : Fin n → X) (f L : X → ℝ) (a : ℝ) (ha : 0 ≤ a) (hL : ∀ x, 0 ≤ L x) (hf : ∀ x, |f x| ≤ a * L x) : Concentration.empiricalNorm S f ≤ a * Concentration.empiricalNorm S L := by unfold Concentration.empiricalNorm rw [← Real.sqrt_sq ha] rw [← Real.sqrt_mul (sq_nonneg a)] apply Real.sqrt_le_sqrt have hsum : (∑ i : Fin n, f (S i) ^ 2) ≤ ∑ i : Fin n, (a * L (S i)) ^ 2 := by apply Finset.sum_le_sum intro i hi rw [sq_le_sq, abs_of_nonneg (mul_nonneg ha (hL (S i)))] exact hf (S i) calc 1 / (n : ℝ) * ∑ i : Fin n, f (S i) ^ 2 ≤ 1 / (n : ℝ) * ∑ i : Fin n, (a * L (S i)) ^ 2 := mul_le_mul_of_nonneg_left hsum (by positivity) _ = a ^ 2 * (1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2) := by simp_rw [mul_pow, ← Finset.mul_sum] ring -
exists_closedBall_net_card_lelemma — A finite-dimensional closed ball has an internal finite net with the standard volumetric cardinality bound, for the ball with center and nonnegative radius at any positive net scale.hypothesesE :θ₀ :Eδ r :ℝhδ :0 ≤ δhr :0 < rProof (Lean source)
lemma exists_closedBall_net_card_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (θ₀ : E) {δ r : ℝ} (hδ : 0 ≤ δ) (hr : 0 < r) : ∃ N : Finset E, (∀ η ∈ N, η ∈ closedBall θ₀ δ) ∧ (∀ θ ∈ closedBall θ₀ δ, ∃ η ∈ N, ‖θ - η‖ < r) ∧ (N.card : ℝ) ≤ (1 + 4 * δ / r) ^ finrank ℝ E := by classical by_cases hδ0 : δ = 0 · subst δ refine ⟨{θ₀}, ?_, ?_, ?_⟩ · intro η hη simpa [Metric.mem_closedBall] using hη · intro θ hθ have hθeq : θ = θ₀ := by simpa [Metric.mem_closedBall] using hθ subst θ exact ⟨θ₀, by simp, by simpa using hr⟩ · simp · have hδpos : 0 < δ := lt_of_le_of_ne hδ (Ne.symm hδ0) let v : ℝ := r / (2 * δ) have hv : 0 < v := div_pos hr (mul_pos (by norm_num) hδpos) obtain ⟨M, hMsub, hMcover, hMcard⟩ := exists_internal_net_card_le E {x : E | ‖x‖ ≤ 1} (by simp) hv let N : Finset E := M.image (fun y => θ₀ + δ • y) refine ⟨N, ?_, ?_, ?_⟩ · intro η hη obtain ⟨y, hyM, rfl⟩ := Finset.mem_image.mp hη rw [Metric.mem_closedBall, dist_eq_norm] rw [add_sub_cancel_left, norm_smul, Real.norm_eq_abs, abs_of_pos hδpos] simpa using mul_le_mul_of_nonneg_left (hMsub y hyM) hδ · intro θ hθ let x : E := δ⁻¹ • (θ - θ₀) have hx : ‖x‖ ≤ 1 := by dsimp [x] rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hδpos] have hθnorm : ‖θ - θ₀‖ ≤ δ := by simpa [Metric.mem_closedBall, dist_eq_norm] using hθ rw [inv_mul_le_one₀ hδpos] exact hθnorm obtain ⟨y, hyM, hxy⟩ := hMcover x hx refine ⟨θ₀ + δ • y, Finset.mem_image.mpr ⟨y, hyM, rfl⟩, ?_⟩ have hscale : θ = θ₀ + δ • x := by dsimp [x] rw [smul_smul, mul_inv_cancel₀ hδ0, one_smul] abel rw [hscale] have hnorm : ‖δ • (x - y)‖ ≤ δ * v := by rw [norm_smul, Real.norm_eq_abs, abs_of_pos hδpos] exact mul_le_mul_of_nonneg_left hxy hδ have hdr : δ * v = r / 2 := by dsimp [v] field_simp calc ‖θ₀ + δ • x - (θ₀ + δ • y)‖ = ‖δ • (x - y)‖ := by congr 1 module _ ≤ δ * v := hnorm _ = r / 2 := hdr _ < r := by linarith · calc (N.card : ℝ) ≤ (M.card : ℝ) := by exact_mod_cast Finset.card_image_le _ ≤ (1 + 2 / v) ^ finrank ℝ E := hMcard _ = (1 + 4 * δ / r) ^ finrank ℝ E := by congr 1 dsimp [v] field_simp ring -
parametric_empiricalDist_lelemma — The empirical distance between two class members is bounded by their parameter distance times the empirical envelope norm on a sample. The scalar class must obey a Lipschitz bound with nonnegative envelope throughout the ball with center and radius, and the two parameters must lie in that ball.hypothesesX E :n :ℕS :Fin n → XF :E → X → ℝL :X → ℝhL :∀ x, 0 ≤ L xθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ x, |F θ x - F η x| ≤ L x * ‖θ - η‖θ :Ehθ :θ ∈ closedBall θ₀ δη :Ehη :η ∈ closedBall θ₀ δconclusionConcentration.empiricalDist S (F θ) (F η) ≤ ‖θ - η‖ * Concentration.empiricalNorm S LProof (Lean source)
lemma parametric_empiricalDist_le {X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (S : Fin n → X) (F : E → X → ℝ) (L : X → ℝ) (hL : ∀ x, 0 ≤ L x) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ x, |F θ x - F η x| ≤ L x * ‖θ - η‖) (θ : E) (hθ : θ ∈ closedBall θ₀ δ) (η : E) (hη : η ∈ closedBall θ₀ δ) : Concentration.empiricalDist S (F θ) (F η) ≤ ‖θ - η‖ * Concentration.empiricalNorm S L := by rw [Concentration.empiricalDist_def] apply empiricalNorm_le_mul S (F θ - F η) L ‖θ - η‖ (norm_nonneg _) hL intro x simpa [Pi.sub_apply, mul_comm] using hLip θ hθ η hη x -
parametric_empirical_totallyBoundedlemma — A scalar function class indexed by a finite-dimensional closed ball is totally bounded in the empirical metric on a sample, when the class has a nonnegative envelope and obeys the corresponding Lipschitz bound on the ball with center, radius, and nonnegative radius proof.hypothesesX E :n :ℕS :Fin n → XF :E → X → ℝL :X → ℝhL :∀ x, 0 ≤ L xθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ x, |F θ x - F η x| ≤ L x * ‖θ - η‖hδ :0 ≤ δconclusionι :closedBall θ₀ δTotallyBounded (Set.univ : Set (Concentration.EmpiricalFunctionSpace (fun θ : ι => F θ.1) S))Proof (Lean source)
lemma parametric_empirical_totallyBounded {X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (S : Fin n → X) (F : E → X → ℝ) (L : X → ℝ) (hL : ∀ x, 0 ≤ L x) (θ₀ : E) (δ : ℝ) (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ x, |F θ x - F η x| ≤ L x * ‖θ - η‖) (hδ : 0 ≤ δ) : let ι := closedBall θ₀ δ TotallyBounded (Set.univ : Set (Concentration.EmpiricalFunctionSpace (fun θ : ι => F θ.1) S)) := by dsimp only classical rw [Metric.totallyBounded_iff] intro r hr let a := Concentration.empiricalNorm S L have ha : 0 ≤ a := by dsimp [a, Concentration.empiricalNorm] exact Real.sqrt_nonneg _ let q : ℝ := r / (a + 1) have hq : 0 < q := div_pos hr (by linarith) obtain ⟨N, hNsub, hNcover, _hNcard⟩ := exists_closedBall_net_card_le θ₀ hδ hq let T : Finset (Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S) := N.attach.image fun y => ⟨⟨y.1, hNsub y.1 y.2⟩⟩ refine ⟨(T : Set _), T.finite_toSet, ?_⟩ intro z hz obtain ⟨η, hηN, hzη⟩ := hNcover z.index.1 z.index.2 let c : Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S := ⟨⟨η, hNsub η hηN⟩⟩ refine Set.mem_iUnion_of_mem c ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr <| Finset.mem_image.mpr ⟨⟨η, hηN⟩, Finset.mem_attach _ _, rfl⟩ · change Concentration.empiricalDist S (F z.index.1) (F η) < r have hd := parametric_empiricalDist_le S F L hL θ₀ hLip z.index.1 z.index.2 η (hNsub η hηN) calc Concentration.empiricalDist S (F z.index.1) (F η) ≤ ‖z.index.1 - η‖ * a := hd _ ≤ q * a := mul_le_mul_of_nonneg_right hzη.le ha _ < r := by dsimp [q] have hden : 0 < a + 1 := by linarith rw [div_mul_eq_mul_div] exact (div_lt_iff₀ hden).2 (by nlinarith) -
parametric_coveringNumber_lelemma — The empirical covering number of a Lipschitz class obeys the finite-dimensional volumetric bound on a sample. The scalar class has a nonnegative envelope and Lipschitz control on the ball with center and nonnegative radius, at positive covering scale.hypothesesX E :n :ℕS :Fin n → XF :E → X → ℝL :X → ℝhL :∀ x, 0 ≤ L xθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖hδ :0 ≤ δx :ℝhx :0 < xconclusionι :closedBall θ₀ δhtot :parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ(Concentration.coveringNumber' htot x : ℝ)≤ (1 + 8 * δ * Concentration.empiricalNorm S L / x) ^ finrank ℝ EProof (Lean source)
lemma parametric_coveringNumber_le {X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (S : Fin n → X) (F : E → X → ℝ) (L : X → ℝ) (hL : ∀ x, 0 ≤ L x) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖) (hδ : 0 ≤ δ) {x : ℝ} (hx : 0 < x) : let ι := closedBall θ₀ δ let htot := parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ (Concentration.coveringNumber' htot x : ℝ) ≤ (1 + 8 * δ * Concentration.empiricalNorm S L / x) ^ finrank ℝ E := by dsimp only classical let a := Concentration.empiricalNorm S L have ha : 0 ≤ a := by dsimp [a, Concentration.empiricalNorm] exact Real.sqrt_nonneg _ by_cases ha0 : a = 0 · let z : Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S := ⟨⟨θ₀, by simp [hδ]⟩⟩ let T : Finset (Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S) := {z} have hcover : (Set.univ : Set (Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S)) ⊆ ⋃ y ∈ T, ball y x := by intro q hq refine Set.mem_iUnion_of_mem z ?_ refine Set.mem_iUnion_of_mem (by simp [T] : z ∈ T) ?_ change Concentration.empiricalDist S (F q.index.1) (F θ₀) < x exact (parametric_empiricalDist_le S F L hL θ₀ hLip q.index.1 q.index.2 θ₀ (Metric.mem_closedBall_self hδ)).trans_lt (by simp [a, ha0, hx]) rw [Concentration.coveringNumber'_eq (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ) hx] calc (find (Concentration.coveringNumber_exists (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ) hx) : ℝ) ≤ (T.card : ℝ) := by exact_mod_cast Nat.find_min' (Concentration.coveringNumber_exists (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ) hx) ⟨T, rfl, hcover⟩ _ = 1 := by simp [T] _ ≤ (1 + 8 * δ * Concentration.empiricalNorm S L / x) ^ finrank ℝ E := by rw [show Concentration.empiricalNorm S L = 0 by simpa [a] using ha0] simp · have hapos : 0 < a := lt_of_le_of_ne ha (Ne.symm ha0) let q : ℝ := x / (2 * a) have hq : 0 < q := div_pos hx (mul_pos (by norm_num) hapos) obtain ⟨N, hNsub, hNcover, hNcard⟩ := exists_closedBall_net_card_le θ₀ hδ hq let T : Finset (Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S) := N.attach.image fun y => ⟨⟨y.1, hNsub y.1 y.2⟩⟩ have hcover : (Set.univ : Set (Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S)) ⊆ ⋃ y ∈ T, ball y x := by intro z hz obtain ⟨η, hηN, hzη⟩ := hNcover z.index.1 z.index.2 let c : Concentration.EmpiricalFunctionSpace (fun θ : closedBall θ₀ δ => F θ.1) S := ⟨⟨η, hNsub η hηN⟩⟩ refine Set.mem_iUnion_of_mem c ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr <| Finset.mem_image.mpr ⟨⟨η, hηN⟩, Finset.mem_attach _ _, rfl⟩ · change Concentration.empiricalDist S (F z.index.1) (F η) < x have hd := parametric_empiricalDist_le S F L hL θ₀ hLip z.index.1 z.index.2 η (hNsub η hηN) calc Concentration.empiricalDist S (F z.index.1) (F η) ≤ ‖z.index.1 - η‖ * a := hd _ < q * a := mul_lt_mul_of_pos_right hzη hapos _ = x / 2 := by dsimp [q]; field_simp _ < x := by linarith rw [Concentration.coveringNumber'_eq (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ) hx] calc (find (Concentration.coveringNumber_exists (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ) hx) : ℝ) ≤ (T.card : ℝ) := by exact_mod_cast Nat.find_min' (Concentration.coveringNumber_exists (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ) hx) ⟨T, rfl, hcover⟩ _ ≤ (N.card : ℝ) := by dsimp [T] exact_mod_cast (Finset.card_image_le.trans_eq Finset.card_attach) _ ≤ (1 + 4 * δ / q) ^ finrank ℝ E := hNcard _ = (1 + 8 * δ * Concentration.empiricalNorm S L / x) ^ finrank ℝ E := by congr 1 dsimp [q, a] field_simp ring
Rademacher 1 core · 2 supporting This module applies conditional Dudley chaining to a finite-dimensional Lipschitz score class, obtaining a samplewise bound in terms of the empirical envelope norm. ★ parametric_empiricalRademacher_le
Conditional Rademacher bounds for Lipschitz parameter classes
This module applies conditional Dudley chaining to a finite-dimensional Lipschitz score class, obtaining a samplewise bound in terms of the empirical envelope norm.
lemma parametric_empiricalRademacher_le reviewed
⚑ flagged
Causalean.Stat
The absolute empirical Rademacher complexity of a centered Lipschitz class is bounded by dimension times radius and empirical envelope norm for positive sample size and sample. The class is centered and has Lipschitz control by a nonnegative envelope on the ball with center and positive radius.
Formal statement
hypotheses
X E :
n :
ℕ
hn :
0 < n
S :
Fin n → X
F :
E → X → ℝ
L :
X → ℝ
hL :
∀ x, 0 ≤ L x
θ₀ :
E
δ :
ℝ
hLip :
∀ θ ∈ closedBall θ₀ δ,
∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖
hzero :
∀ x, F θ₀ x = 0
hδ :
0 < δ
conclusion
empiricalRademacherComplexity n (fun θ : closedBall θ₀ δ => F θ.1) S
Proof (Lean source)
lemma parametric_empiricalRademacher_le
{X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{n : ℕ} (hn : 0 < n) (S : Fin n → X) (F : E → X → ℝ) (L : X → ℝ)
(hL : ∀ x, 0 ≤ L x)
(θ₀ : E) {δ : ℝ}
(hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z,
|F θ z - F η z| ≤ L z * ‖θ - η‖)
(hzero : ∀ x, F θ₀ x = 0)
(hδ : 0 < δ) :
empiricalRademacherComplexity n
(fun θ : closedBall θ₀ δ => F θ.1) S ≤
96 * (finrank ℝ E + 1) * δ *
Concentration.empiricalNorm S L / sqrt (n : ℝ) := by
classical
let FB : closedBall θ₀ δ → X → ℝ := fun θ => F θ.1
let i₀ : closedBall θ₀ δ := ⟨θ₀, by simp [hδ.le]⟩
letI : Nonempty (closedBall θ₀ δ) := ⟨i₀⟩
let a := Concentration.empiricalNorm S L
have ha : 0 ≤ a := by dsimp [a, Concentration.empiricalNorm]; positivity
by_cases ha0 : a = 0
· have hsampleZero : ∀ θ : closedBall θ₀ δ, ∀ k, FB θ (S k) = 0 := by
intro θ k
have hinside : (n : ℝ)⁻¹ * ∑ i : Fin n, L (S i) ^ 2 = 0 := by
have hsqrt : sqrt ((n : ℝ)⁻¹ * ∑ i : Fin n, L (S i) ^ 2) = 0 := by
simpa [a, Concentration.empiricalNorm] using ha0
exact (Real.sqrt_eq_zero (by positivity)).mp hsqrt
have hsum : ∑ i : Fin n, L (S i) ^ 2 = 0 := by
rcases mul_eq_zero.mp hinside with hinv | hsum
· exact False.elim (inv_ne_zero (by exact_mod_cast hn.ne') hinv)
· exact hsum
have hterm := (Finset.sum_eq_zero_iff_of_nonneg
(fun i _ => sq_nonneg (L (S i)))).mp hsum k (by simp)
have hLzero : L (S k) = 0 := sq_eq_zero_iff.mp hterm
have hd := hLip θ.1 θ.2 θ₀ (Metric.mem_closedBall_self hδ.le) (S k)
have : |F θ.1 (S k)| ≤ 0 := by simpa [hzero, hLzero] using hd
exact abs_eq_zero.mp (le_antisymm this (abs_nonneg _))
have hcongr := Concentration.empiricalRademacherComplexity_congr_sample n FB
(fun _ _ => 0) S (fun θ k => hsampleZero θ k)
rw [hcongr]
unfold empiricalRademacherComplexity
simp [ha0, a]
· have hapos : 0 < Concentration.empiricalNorm S L := by
simpa [a] using lt_of_le_of_ne ha (Ne.symm ha0)
have hM : ∀ θ : closedBall θ₀ δ, ∀ k,
|FB θ (S k)| ≤ δ * ∑ i : Fin n, L (S i) := by
intro θ k
have hb := hLip θ.1 θ.2 θ₀ (Metric.mem_closedBall_self hδ.le) (S k)
have hθ : ‖θ.1 - θ₀‖ ≤ δ := by
have hp := θ.2
rw [Metric.mem_closedBall, dist_eq_norm] at hp
exact hp
calc
|FB θ (S k)| ≤ L (S k) * ‖θ.1 - θ₀‖ := by simpa [FB, hzero] using hb
_ ≤ L (S k) * δ := mul_le_mul_of_nonneg_left hθ (hL _)
_ ≤ δ * ∑ i : Fin n, L (S i) := by
rw [mul_comm]
gcongr
exact Finset.single_le_sum (fun i _ => hL (S i)) (by simp)
have habs := empiricalRademacherComplexity_le_signed_add_neg_of_zero_sample
FB i₀ (by simp [FB, i₀, hzero]) S
(mul_nonneg hδ.le (Finset.sum_nonneg fun i _ => hL (S i))) hM
have hsigned := parametric_empiricalRademacher_without_abs_le
hn S F L hL θ₀ hLip hzero hδ hapos
have hLipNeg : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z,
|(-F θ z) - (-F η z)| ≤ L z * ‖θ - η‖ := by
intro θ hθ η hη z
rw [show (-F θ z) - (-F η z) = -(F θ z - F η z) by ring, abs_neg]
exact hLip θ hθ η hη z
have hsignedNeg := parametric_empiricalRademacher_without_abs_le
hn S (fun θ x => -F θ x) L hL θ₀ hLipNeg (by simp [hzero]) hδ hapos
calc
empiricalRademacherComplexity n FB S
≤ empiricalRademacherComplexity_without_abs n FB S +
empiricalRademacherComplexity_without_abs n (fun θ x => -FB θ x) S := habs
_ ≤ 96 * (finrank ℝ E + 1) * δ * a /
sqrt (n : ℝ) := by
rw [show (96 : ℝ) = 48 + 48 by norm_num]
simpa [FB, a, add_mul, add_div] using add_le_add hsigned hsignedNeg
_ = 96 * (finrank ℝ E + 1) * δ *
Concentration.empiricalNorm S L / sqrt (n : ℝ) := rfl
2 supporting declarations (lemmas, instances)
-
empiricalRademacherComplexity_le_signed_add_neg_of_zero_samplelemma — The absolute Rademacher complexity is bounded by the sum of the positive and negative signed complexities for a function class containing a pointwise-zero member, when the class is uniformly bounded on the sample by a nonnegative bound.hypothesesX ι :Type*Nonempty ιH :ι → X → ℝi₀ :ιhzero :∀ x, H i₀ x = 0n :ℕS :Fin n → XM :ℝhM0 :0 ≤ MhM :∀ i k, |H i (S k)| ≤ MconclusionempiricalRademacherComplexity n H S≤ empiricalRademacherComplexity_without_abs n H S+ empiricalRademacherComplexity_without_abs n (fun i x => -H i x) SProof (Lean source)
lemma empiricalRademacherComplexity_le_signed_add_neg_of_zero_sample {X ι : Type*} [Nonempty ι] (H : ι → X → ℝ) (i₀ : ι) (hzero : ∀ x, H i₀ x = 0) {n : ℕ} (S : Fin n → X) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ i k, |H i (S k)| ≤ M) : empiricalRademacherComplexity n H S ≤ empiricalRademacherComplexity_without_abs n H S + empiricalRademacherComplexity_without_abs n (fun i x => -H i x) S := by classical unfold empiricalRademacherComplexity empiricalRademacherComplexity_without_abs rw [← mul_add, ← Finset.sum_add_distrib] refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun τ _ => ?_) (by positivity) let z : ι → ℝ := fun i => (n : ℝ)⁻¹ * ∑ k : Fin n, (τ k : ℝ) * H i (S k) have hz0 : z i₀ = 0 := by simp [z, hzero] have hzabs : ∀ i, |z i| ≤ M := by intro i calc |z i| ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, |H i (S k)| := by dsimp [z] rw [abs_mul, abs_of_nonneg (inv_nonneg.mpr (Nat.cast_nonneg _))] gcongr exact (Finset.abs_sum_le_sum_abs _ _).trans_eq (by congr 1 ext k simp) _ ≤ (n : ℝ)⁻¹ * ∑ _k : Fin n, M := by gcongr with k exact hM i k _ ≤ M := by by_cases hn : n = 0 · subst n simp [hM0] · simp [Nat.cast_ne_zero.mpr hn] have hbddAbs : BddAbove (range fun i => |z i|) := ⟨M, by rintro _ ⟨i, rfl⟩; exact hzabs i⟩ have hbdd : BddAbove (range z) := ⟨M, by rintro _ ⟨i, rfl⟩; exact (le_abs_self _).trans (hzabs i)⟩ have hbddNeg : BddAbove (range fun i => -z i) := ⟨M, by rintro _ ⟨i, rfl⟩; exact (neg_le_abs _).trans (hzabs i)⟩ have hsup0 : 0 ≤ ⨆ i, z i := by rw [← hz0]; exact le_ciSup hbdd i₀ have hsupNeg0 : 0 ≤ ⨆ i, -z i := by rw [← show -z i₀ = 0 by rw [hz0]; simp] exact le_ciSup hbddNeg i₀ have hpoint : (⨆ i, |z i|) ≤ (⨆ i, z i) + (⨆ i, -z i) := by refine ciSup_le fun i => ?_ by_cases hi : 0 ≤ z i · rw [abs_of_nonneg hi] linarith [le_ciSup hbdd i] · rw [abs_of_neg (lt_of_not_ge hi)] linarith [le_ciSup hbddNeg i] have hneg : (⨆ i, -z i) = ⨆ i, (n : ℝ)⁻¹ * ∑ k : Fin n, (τ k : ℝ) * (-H i (S k)) := by refine iSup_congr fun i => ?_ calc -z i = (n : ℝ)⁻¹ * (-(∑ k : Fin n, (τ k : ℝ) * H i (S k))) := by simp only [z] ring _ = (n : ℝ)⁻¹ * ∑ k : Fin n, -((τ k : ℝ) * H i (S k)) := by rw [Finset.sum_neg_distrib] _ = (n : ℝ)⁻¹ * ∑ k : Fin n, (τ k : ℝ) * (-H i (S k)) := by congr 1 refine Finset.sum_congr rfl fun k _ => by ring simpa [z, hneg] using hpoint -
parametric_empiricalRademacher_without_abs_lelemma — The signed empirical Rademacher complexity of a centered Lipschitz class obeys the finite-dimensional chaining bound for positive sample size and sample. The class is centered and has Lipschitz control by a nonnegative envelope on the ball with center and positive radius, whose empirical envelope norm is positive.hypothesesX E :n :ℕhn :0 < nS :Fin n → XF :E → X → ℝL :X → ℝhL :∀ x, 0 ≤ L xθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖hzero :∀ x, F θ₀ x = 0hδ :0 < δha :0 < Concentration.empiricalNorm S LconclusionempiricalRademacherComplexity_without_abs n (fun θ : closedBall θ₀ δ => F θ.1) SProof (Lean source)
lemma parametric_empiricalRademacher_without_abs_le {X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (hn : 0 < n) (S : Fin n → X) (F : E → X → ℝ) (L : X → ℝ) (hL : ∀ x, 0 ≤ L x) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖) (hzero : ∀ x, F θ₀ x = 0) (hδ : 0 < δ) (ha : 0 < Concentration.empiricalNorm S L) : empiricalRademacherComplexity_without_abs n (fun θ : closedBall θ₀ δ => F θ.1) S ≤ 48 * (finrank ℝ E + 1) * δ * Concentration.empiricalNorm S L / sqrt (n : ℝ) := by classical let FB : closedBall θ₀ δ → X → ℝ := fun θ => F θ.1 let a := Concentration.empiricalNorm S L have hapos : 0 < a := by simpa [a] using ha let i₀ : closedBall θ₀ δ := ⟨θ₀, by simp [hδ.le]⟩ letI : Nonempty (closedBall θ₀ δ) := ⟨i₀⟩ have hnorm : ∀ θ : closedBall θ₀ δ, Concentration.empiricalNorm S (FB θ) ≤ δ * a := by intro θ apply empiricalNorm_le_mul S (FB θ) L δ hδ.le hL intro x have hb := hLip θ.1 θ.2 θ₀ (Metric.mem_closedBall_self hδ.le) x have hθ : ‖θ.1 - θ₀‖ ≤ δ := by have hp := θ.2 rw [Metric.mem_closedBall, dist_eq_norm] at hp exact hp simpa [FB, hzero, mul_comm] using hb.trans (mul_le_mul_of_nonneg_left hθ (hL x)) apply le_of_forall_pos_le_add intro ζ hζ let ε := min (δ * a / 2) (ζ / 4) have hε : 0 < ε := lt_min (by positivity) (by positivity) have hδa : 0 < δ * a := mul_pos hδ hapos have hεR : ε ≤ δ * a := (min_le_left _ _).trans (by linarith) have hdudley := Concentration.dudley_entropy_integral_bound (F := FB) (c := 2 * (δ * a)) hε (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ.le) hn (fun θ => (hnorm θ).trans (by linarith [hδa])) (by have hm := min_le_left (δ * a / 2) (ζ / 4) change ε < (2 * (δ * a)) / 2 rw [show (2 * (δ * a)) / 2 = δ * a by ring] exact lt_of_le_of_lt hm (by linarith)) have hint := parametric_entropyIntegral_le S F L hL θ₀ hLip hδ hapos hε hεR have hεζ : 4 * ε ≤ ζ := by dsimp [ε] linarith [min_le_right (δ * a / 2) (ζ / 4)] calc empiricalRademacherComplexity_without_abs n FB S ≤ 4 * ε + 12 / sqrt (n : ℝ) * (∫ x in ε..(δ * a), sqrt (log (Concentration.coveringNumber' (parametric_empirical_totallyBounded S F L hL θ₀ δ hLip hδ.le) x))) := by simpa [FB, a] using hdudley _ ≤ 4 * ε + 12 / sqrt (n : ℝ) * (4 * (finrank ℝ E + 1) * (δ * a)) := by gcongr _ ≤ 48 * (finrank ℝ E + 1) * δ * a / sqrt (n : ℝ) + ζ := by have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 (by exact_mod_cast hn) rw [div_eq_mul_inv, div_eq_mul_inv] nlinarith [hεζ, inv_pos.mpr hsqrt, show (0 : ℝ) ≤ finrank ℝ E by positivity]
Sample 1 core · 0 supporting This module transports the finite-product expected-supremum inequality to the sample vector generated by an IIDSample. ★ parametricEmpProcSup_expected_le
IID-sample form of the Lipschitz empirical-process bound
This module transports the finite-product expected-supremum inequality to the
sample vector generated by an IIDSample.
theorem parametricEmpProcSup_expected_le reviewed
⚑ flagged
Causalean.Stat.IIDSample
The expected local empirical-process supremum along an i.i.d. sample obeys the finite-dimensional Lipschitz bound for an i.i.d. sample of positive size. The result assumes a measurable Lipschitz score class with a square-integrable nonnegative envelope, on a positive-radius parameter ball where the Lipschitz bound holds.
Formal statement
hypotheses
Ω X E V :
S :
IIDSample Ω X μ P
n :
ℕ
hn :
0 < n
ψ :
E → X → V
L :
X → ℝ
hψmeas :
∀ θ, Measurable (ψ θ)
hLmeas :
hL :
∀ x, 0 ≤ L x
hL2 :
Integrable (fun x => L x ^ 2) P
θ₀ :
E
δ :
ℝ
hLip :
∀ θ ∈ closedBall θ₀ δ,
∀ η ∈ closedBall θ₀ δ, ∀ z, ‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖
hδ :
0 < δ
conclusion
∫ ω, parametricEmpProcSup P ψ θ₀ hδ.le n (fun k : Fin n => S.Z k ω) ∂μ
≤ lipschitzParametricConstant E V * δ * sqrt (∫ x, L x ^ 2 ∂P)
Proof (Lean source)
theorem IIDSample.parametricEmpProcSup_expected_le
{Ω X E V : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
[NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
[MeasurableSpace V] [BorelSpace V]
{μ : Measure Ω} {P : Measure X} (S : IIDSample Ω X μ P)
{n : ℕ} (hn : 0 < n) (ψ : E → X → V) (L : X → ℝ)
(hψmeas : ∀ θ, Measurable (ψ θ)) (hLmeas : Measurable L)
(hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P)
(θ₀ : E) {δ : ℝ}
(hLip : ∀ θ ∈ closedBall θ₀ δ, ∀ η ∈ closedBall θ₀ δ, ∀ z,
‖ψ θ z - ψ η z‖ ≤ L z * ‖θ - η‖)
(hδ : 0 < δ) :
∫ ω, parametricEmpProcSup P ψ θ₀ hδ.le n (fun k : Fin n => S.Z k ω) ∂μ ≤
lipschitzParametricConstant E V * δ * sqrt (∫ x, L x ^ 2 ∂P) := by
haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
let W : Ω → (Fin n → X) := fun ω k => S.Z k ω
have hWmeas : Measurable W := iidSample_finN_measurable S n
have hUmeas : Measurable (fun T : Fin n → X =>
parametricEmpProcSup P ψ θ₀ hδ.le n T) :=
parametricEmpProcSup_measurable P ψ θ₀ hδ.le n hψmeas
rw [← MeasureTheory.integral_map hWmeas.aemeasurable hUmeas.aestronglyMeasurable,
iidSample_finN_pushforward S n]
exact parametricEmpProcSup_expected_le
P hn ψ L hψmeas hLmeas hL hL2 θ₀ hLip hδ
Scalar 1 core · 4 supporting This module combines symmetrization, conditional chaining, and envelope truncation to obtain an expected uniform-deviation inequality under only a square-integrable envelope. ★ scalar_parametric_expected_average_le
Expected scalar deviations for Lipschitz parameter classes
This module combines symmetrization, conditional chaining, and envelope truncation to obtain an expected uniform-deviation inequality under only a square-integrable envelope.
theorem scalar_parametric_expected_average_le reviewed
⚑ flagged
Causalean.Stat
The expected uniform empirical-average deviation of a Lipschitz scalar class is bounded by dimension times radius and the population envelope norm under a population probability law at positive sample size. The measurable score class is centered and Lipschitz on the parameter ball, with a measurable, nonnegative, square-integrable envelope.
Formal statement
hypotheses
X E :
P :
n :
ℕ
hn :
0 < n
F :
E → X → ℝ
L :
X → ℝ
hFmeas :
∀ θ, Measurable (F θ)
hLmeas :
hL :
∀ x, 0 ≤ L x
hL2 :
Integrable (fun x => L x ^ 2) P
θ₀ :
E
δ :
ℝ
hLip :
∀ θ ∈ closedBall θ₀ δ,
∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖
hzero :
∀ x, F θ₀ x = 0
hδ :
0 < δ
conclusion
∫ S : Fin n → X, uniformDeviation n ((fun θ : closedBall θ₀ δ => F θ.1) ∘ closedBallDenseSeq θ₀ hδ.le) P id S ∂Measure.pi (fun _ : Fin n => P)
Proof (Lean source)
theorem scalar_parametric_expected_average_le
{X E : Type*} [MeasurableSpace X]
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
(P : Measure X) [IsProbabilityMeasure P]
{n : ℕ} (hn : 0 < n) (F : E → X → ℝ) (L : X → ℝ)
(hFmeas : ∀ θ, Measurable (F θ)) (hLmeas : Measurable L)
(hL : ∀ x, 0 ≤ L x)
(hL2 : Integrable (fun x => L x ^ 2) P)
(θ₀ : E) {δ : ℝ}
(hLip : ∀ θ ∈ Metric.closedBall θ₀ δ, ∀ η ∈ Metric.closedBall θ₀ δ, ∀ z,
|F θ z - F η z| ≤ L z * ‖θ - η‖)
(hzero : ∀ x, F θ₀ x = 0)
(hδ : 0 < δ) :
∫ S : Fin n → X,
uniformDeviation n
((fun θ : Metric.closedBall θ₀ δ => F θ.1) ∘
closedBallDenseSeq θ₀ hδ.le) P id S
∂Measure.pi (fun _ : Fin n => P) ≤
192 * (finrank ℝ E + 1) * δ *
sqrt (∫ x, L x ^ 2 ∂P) / sqrt (n : ℝ) := by
classical
let B := Metric.closedBall θ₀ δ
let θseq : ℕ → B := closedBallDenseSeq θ₀ hδ.le
let F0 : ℕ → X → ℝ := (fun θ : B => F θ.1) ∘ θseq
let moment := ∫ x, L x ^ 2 ∂P
have hmoment : 0 ≤ moment := integral_nonneg fun x => sq_nonneg (L x)
have hLint : Integrable L P := by
apply Integrable.mono' ((integrable_const (1 : ℝ)).add hL2)
hLmeas.aestronglyMeasurable
filter_upwards with x
change |L x| ≤ 1 + L x ^ 2
rw [abs_of_nonneg (hL x)]
nlinarith [sq_nonneg (L x - 1 / 2)]
apply le_of_forall_pos_le_add
intro ζ hζ
let M := 1 + 2 * δ * moment / ζ
have hM : 0 < M := by dsimp [M]; positivity
let keep : Set X := {x | L x ≤ M}
have hkeep : MeasurableSet keep := measurableSet_le hLmeas measurable_const
let LT : X → ℝ := fun x => if x ∈ keep then L x else 0
let T : X → ℝ := fun x => if x ∈ keep then 0 else L x
let FT : E → X → ℝ := fun θ x => if x ∈ keep then F θ x else 0
let H0 : ℕ → X → ℝ := (fun θ : B => FT θ.1) ∘ θseq
have hLTmeas : Measurable LT := Measurable.ite hkeep hLmeas measurable_const
have hTmeas : Measurable T := Measurable.ite hkeep measurable_const hLmeas
have hFTmeas : ∀ θ, Measurable (FT θ) := fun θ =>
Measurable.ite hkeep (hFmeas θ) measurable_const
have hLT : ∀ x, 0 ≤ LT x := by intro x; simp only [LT]; split <;> simp [hL]
have hT : ∀ x, 0 ≤ T x := by intro x; simp only [T]; split <;> simp [hL]
have hLTle : ∀ x, LT x ≤ M := by
intro x
simp only [LT]
split
· simpa [keep] using ‹x ∈ keep›
· exact hM.le
have hLTsq : Integrable (fun x => LT x ^ 2) P := by
apply Integrable.mono' hL2 (hLTmeas.pow_const 2).aestronglyMeasurable
filter_upwards with x
simp only [LT]
split <;> simp [sq_nonneg]
have hTint : Integrable T P := by
apply Integrable.mono' hLint hTmeas.aestronglyMeasurable
filter_upwards with x
simp only [T]
split <;> simp [hL, abs_of_nonneg]
have hLipT : ∀ θ ∈ Metric.closedBall θ₀ δ, ∀ η ∈ Metric.closedBall θ₀ δ, ∀ z,
|FT θ z - FT η z| ≤ LT z * ‖θ - η‖ := by
intro θ hθ η hη z
simp only [FT, LT]
split
· exact hLip θ hθ η hη z
· simp
have hzeroT : ∀ x, FT θ₀ x = 0 := by
intro x
simp [FT, hzero]
have htrunc := scalar_parametric_expected_average_le_of_bounded
P hn FT LT hFTmeas hLTmeas hLT hLTsq θ₀ hLipT hzeroT hδ hM.le hLTle
have hmomentT : (∫ x, LT x ^ 2 ∂P) ≤ moment := by
apply integral_mono hLTsq hL2
intro x
simp only [LT]
split <;> simp [sq_nonneg]
have htrunc' :
∫ S : Fin n → X, uniformDeviation n H0 P id S
∂Measure.pi (fun _ : Fin n => P) ≤
192 * (finrank ℝ E + 1) * δ *
sqrt moment / sqrt (n : ℝ) := by
calc
_ ≤ 192 * (finrank ℝ E + 1) * δ *
sqrt (∫ x, LT x ^ 2 ∂P) / sqrt (n : ℝ) := by
simpa [H0, θseq, B] using htrunc
_ ≤ _ := by
gcongr
have htail : (∫ x, T x ∂P) ≤ moment / M := by
have hdom : ∀ x, T x ≤ L x ^ 2 / M := by
intro x
simp only [T]
split
· positivity
· have hx : M < L x := lt_of_not_ge (by simpa [keep] using ‹x ∉ keep›)
apply (le_div_iff₀ hM).2
nlinarith [hL x]
have hright : Integrable (fun x => L x ^ 2 / M) P := hL2.div_const M
calc
_ ≤ ∫ x, L x ^ 2 / M ∂P := integral_mono hTint hright hdom
_ = moment / M := by rw [integral_div]
have htailSmall : 2 * δ * (∫ x, T x ∂P) < ζ := by
have hfrac : 2 * δ * (moment / M) < ζ := by
rw [show 2 * δ * (moment / M) = (2 * δ * moment) / M by ring]
apply (div_lt_iff₀ hM).2
dsimp [M]
field_simp [ne_of_gt hζ]
nlinarith [hζ]
exact (mul_le_mul_of_nonneg_left htail
(mul_nonneg (by norm_num) hδ.le)).trans_lt hfrac
let Td : X → ℝ := fun x => δ * T x
have hTdmeas : Measurable Td := hTmeas.const_mul δ
have hTdint : Integrable Td P := hTint.const_mul δ
have hTd : ∀ x, 0 ≤ Td x := fun x => mul_nonneg hδ.le (hT x)
have hH0meas : ∀ k, Measurable (H0 k) := fun k => hFTmeas _
have hF0meas : ∀ k, Measurable (F0 k) := fun k => hFmeas _
have hH0bound : ∀ k x, |H0 k x| ≤ δ * M := by
intro k x
simp only [H0, Function.comp_apply, FT]
split
· let θ : B := θseq k
have hp := θ.2
rw [Metric.mem_closedBall, dist_eq_norm] at hp
calc
|F θ.1 x| ≤ L x * ‖θ.1 - θ₀‖ := by
simpa [hzero] using hLip θ.1 θ.2 θ₀ (Metric.mem_closedBall_self hδ.le) x
_ ≤ M * δ := mul_le_mul (by simpa [keep] using ‹x ∈ keep›) hp (norm_nonneg _) hM.le
_ = δ * M := by ring
· simp [mul_nonneg hδ.le hM.le]
have hdiff : ∀ k x, |F0 k x - H0 k x| ≤ Td x := by
intro k x
simp only [F0, H0, Function.comp_apply, FT, Td, T]
split
· simp
· let θ : B := θseq k
have hp := θ.2
rw [Metric.mem_closedBall, dist_eq_norm] at hp
calc
|F θ.1 x - 0| ≤ L x * ‖θ.1 - θ₀‖ := by
simpa [hzero] using hLip θ.1 θ.2 θ₀ (Metric.mem_closedBall_self hδ.le) x
_ ≤ L x * δ := mul_le_mul_of_nonneg_left hp (hL x)
_ = δ * L x := by ring
have hcomp (S : Fin n → X) : uniformDeviation n F0 P id S ≤
uniformDeviation n H0 P id S +
((n : ℝ)⁻¹ * ∑ k : Fin n, Td (S k) + ∫ x, Td x ∂P) :=
uniformDeviation_le_add_envelope P hn F0 H0 Td hF0meas hH0meas
hTdint hH0bound hdiff S
have hHdevMeas : Measurable (fun S : Fin n → X => uniformDeviation n H0 P id S) :=
uniformDeviation_measurable id hH0meas
have hHdevInt : Integrable (fun S : Fin n → X => uniformDeviation n H0 P id S)
(Measure.pi (fun _ : Fin n => P)) := by
apply Integrable.of_bound hHdevMeas.aestronglyMeasurable (2 * (δ * M))
filter_upwards with S
rw [Real.norm_eq_abs, abs_of_nonneg (by
unfold uniformDeviation
exact Real.iSup_nonneg fun k => abs_nonneg _)]
unfold uniformDeviation
simp only [id_eq]
apply ciSup_le
intro k
have hkint : Integrable (H0 k) P := Integrable.of_bound
(hH0meas k).aestronglyMeasurable (δ * M)
(ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hH0bound k x)
have havg : |(n : ℝ)⁻¹ * ∑ i : Fin n, H0 k (S i)| ≤ δ * M := by
rw [abs_mul, abs_of_pos (inv_pos.mpr (by exact_mod_cast hn))]
calc
_ ≤ (n : ℝ)⁻¹ * ∑ i : Fin n, |H0 k (S i)| := by
gcongr; exact Finset.abs_sum_le_sum_abs _ _
_ ≤ (n : ℝ)⁻¹ * ∑ _i : Fin n, (δ * M) := by gcongr with i; exact hH0bound k (S i)
_ = δ * M := by simp [hn.ne']
have hint : |∫ x, H0 k x ∂P| ≤ δ * M := by
calc
_ ≤ ∫ x, |H0 k x| ∂P := abs_integral_le_integral_abs
_ ≤ ∫ _x, δ * M ∂P := integral_mono hkint.abs (integrable_const _) (hH0bound k)
_ = δ * M := by simp
exact (abs_sub _ _).trans (by linarith)
have hTdcoord (k : Fin n) : Integrable (fun S : Fin n → X => Td (S k))
(Measure.pi (fun _ : Fin n => P)) := by
change Integrable (Td ∘ (fun S : Fin n → X => S k)) _
exact ((measurePreserving_eval (fun _ : Fin n => P) k).integrable_comp
hTdint.aestronglyMeasurable).2 hTdint
have hTdavgInt : Integrable (fun S : Fin n → X =>
(n : ℝ)⁻¹ * ∑ k : Fin n, Td (S k)) (Measure.pi (fun _ : Fin n => P)) :=
(integrable_finsetSum univ fun k _ => hTdcoord k).const_mul _
have hTdconstInt : Integrable (fun _S : Fin n → X => ∫ x, Td x ∂P)
(Measure.pi (fun _ : Fin n => P)) := integrable_const _
have herrInt : Integrable (fun S : Fin n → X =>
(n : ℝ)⁻¹ * ∑ k : Fin n, Td (S k) + ∫ x, Td x ∂P)
(Measure.pi (fun _ : Fin n => P)) := hTdavgInt.add hTdconstInt
have hFdevMeas : Measurable (fun S : Fin n → X => uniformDeviation n F0 P id S) :=
uniformDeviation_measurable id hF0meas
have hFdevInt : Integrable (fun S : Fin n → X => uniformDeviation n F0 P id S)
(Measure.pi (fun _ : Fin n => P)) := by
apply Integrable.mono' (hHdevInt.add herrInt) hFdevMeas.aestronglyMeasurable
filter_upwards with S
rw [Real.norm_eq_abs, abs_of_nonneg (by
unfold uniformDeviation
exact Real.iSup_nonneg fun k => abs_nonneg _)]
exact hcomp S
have hIntComp := integral_mono hFdevInt (hHdevInt.add herrInt) hcomp
have herrEval :
(∫ S : Fin n → X,
((n : ℝ)⁻¹ * ∑ k : Fin n, Td (S k) + ∫ x, Td x ∂P)
∂Measure.pi (fun _ : Fin n => P)) = 2 * δ * ∫ x, T x ∂P := by
rw [integral_add hTdavgInt hTdconstInt, integral_const, integral_const_mul,
integral_finsetSum univ (fun k _ => hTdcoord k)]
simp_rw [integral_comp_eval (μ := fun _ : Fin n => P) (i := _) hTdint.aestronglyMeasurable]
rw [show (∫ x, Td x ∂P) = δ * ∫ x, T x ∂P by
simp [Td, integral_const_mul]]
simp [hn.ne']
ring
calc
∫ S : Fin n → X, uniformDeviation n F0 P id S
∂Measure.pi (fun _ : Fin n => P)
≤ (∫ S : Fin n → X, uniformDeviation n H0 P id S
∂Measure.pi (fun _ : Fin n => P)) +
∫ S : Fin n → X,
((n : ℝ)⁻¹ * ∑ k : Fin n, Td (S k) + ∫ x, Td x ∂P)
∂Measure.pi (fun _ : Fin n => P) := by
simpa [integral_add hHdevInt herrInt] using hIntComp
_ ≤ 192 * (finrank ℝ E + 1) * δ * sqrt moment /
sqrt (n : ℝ) + 2 * δ * ∫ x, T x ∂P := by
rw [herrEval]
gcongr
_ ≤ 192 * (finrank ℝ E + 1) * δ * sqrt moment /
sqrt (n : ℝ) + ζ := by linarith
_ = _ := by rfl
4 supporting declarations (lemmas, instances)
-
expected_empiricalNorm_lelemma — The expected empirical envelope norm is at most its population root second moment under a population probability law, for positive sample size and a measurable, square-integrable envelope.hypothesesProof (Lean source)
lemma expected_empiricalNorm_le {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (L : X → ℝ) (hLmeas : Measurable L) (hL2 : Integrable (fun x => L x ^ 2) P) : ∫ S : Fin n → X, Concentration.empiricalNorm S L ∂Measure.pi (fun _ : Fin n => P) ≤ sqrt (∫ x, L x ^ 2 ∂P) := by let Q : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => P) let g : (Fin n → X) → ℝ := fun S => Concentration.empiricalNorm S L have hgmeas : Measurable g := by dsimp [g, Concentration.empiricalNorm] fun_prop have hgsq_eq : (fun S => g S ^ 2) = fun S => 1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2 := by funext S dsimp [g, Concentration.empiricalNorm] rw [Real.sq_sqrt (by positivity)] have hcoord (i : Fin n) : Integrable (fun S : Fin n → X => L (S i) ^ 2) Q := by change Integrable ((fun x => L x ^ 2) ∘ (Function.eval i)) Q exact ((measurePreserving_eval (fun _ : Fin n => P) i).integrable_comp hL2.aestronglyMeasurable).2 hL2 have hgsq : Integrable (fun S => g S ^ 2) Q := by rw [hgsq_eq] exact (integrable_finsetSum univ fun i _ => hcoord i).const_mul _ have hnonneg : ∀ S, 0 ≤ g S := by intro S dsimp [g, Concentration.empiricalNorm] positivity have hgsqnorm : Integrable (fun S => ‖g S‖ ^ 2) Q := by simpa only [Real.norm_eq_abs, abs_of_nonneg (hnonneg _)] using hgsq have hcs := Concentration.HilbertEmpiricalMean.integral_norm_le_sqrt_integral_norm_sq Q g hgmeas.stronglyMeasurable hgsqnorm have hleft : (∫ S, ‖g S‖ ∂Q) = ∫ S, g S ∂Q := by apply integral_congr_ae filter_upwards with S simp [Real.norm_eq_abs, abs_of_nonneg (hnonneg S)] have hcoord_int (i : Fin n) : (∫ S : Fin n → X, L (S i) ^ 2 ∂Q) = ∫ x, L x ^ 2 ∂P := by exact integral_comp_eval (μ := fun _ : Fin n => P) (i := i) hL2.aestronglyMeasurable have hright : (∫ S, ‖g S‖ ^ 2 ∂Q) = ∫ x, L x ^ 2 ∂P := by simp_rw [Real.norm_eq_abs, abs_of_nonneg (hnonneg _)] rw [hgsq_eq, integral_const_mul, integral_finsetSum univ (fun i _ => hcoord i)] simp_rw [hcoord_int] simp [hn.ne'] rw [hleft, hright] at hcs simpa [Q, g] using hcs -
empiricalNorm_integrablelemma — The empirical envelope norm is integrable under the product law for positive sample size when the envelope is measurable and square-integrable under the population probability law.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma empiricalNorm_integrable {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (L : X → ℝ) (hLmeas : Measurable L) (hL2 : Integrable (fun x => L x ^ 2) P) : Integrable (fun S : Fin n → X => Concentration.empiricalNorm S L) (Measure.pi (fun _ : Fin n => P)) := by let Q : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => P) let g : (Fin n → X) → ℝ := fun S => Concentration.empiricalNorm S L have hgmeas : Measurable g := by dsimp [g, Concentration.empiricalNorm] fun_prop have hcoord (i : Fin n) : Integrable (fun S : Fin n → X => L (S i) ^ 2) Q := by change Integrable ((fun x => L x ^ 2) ∘ (Function.eval i)) Q exact ((measurePreserving_eval (fun _ : Fin n => P) i).integrable_comp hL2.aestronglyMeasurable).2 hL2 have hsq : Integrable (fun S : Fin n → X => 1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2) Q := (integrable_finsetSum univ fun i _ => hcoord i).const_mul _ have hdom : ∀ S, ‖g S‖ ≤ 1 + 1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2 := by intro S have hu : 0 ≤ 1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2 := by positivity have hsqrt : sqrt (1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2) ≤ 1 + 1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2 := by nlinarith [Real.sq_sqrt hu, Real.sqrt_nonneg (1 / (n : ℝ) * ∑ i : Fin n, L (S i) ^ 2)] simpa [g, Concentration.empiricalNorm, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] using hsqrt exact Integrable.mono' ((integrable_const (1 : ℝ)).add hsq) hgmeas.aestronglyMeasurable (ae_of_all _ hdom) -
scalar_parametric_expected_average_le_of_boundedtheorem — The expected uniform empirical-average deviation of a bounded Lipschitz class satisfies the finite-dimensional maximal inequality under a population probability law at positive sample size. The measurable class is centered and Lipschitz on the parameter ball, with a measurable, nonnegative, square-integrable envelope that is bounded by a nonnegative constant.hypothesesX E :P :n :ℕhn :0 < nF :E → X → ℝL :X → ℝhFmeas :∀ θ, Measurable (F θ)hLmeas :hL :∀ x, 0 ≤ L xhL2 :Integrable (fun x => L x ^ 2) Pθ₀ :Eδ :ℝhLip :∀ θ ∈ closedBall θ₀ δ,∀ η ∈ closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖hzero :∀ x, F θ₀ x = 0M :ℝhδ :0 < δhM :0 ≤ MhLM :∀ x, L x ≤ Mconclusion∫ S : Fin n → X, uniformDeviation n ((fun θ : closedBall θ₀ δ => F θ.1) ∘ closedBallDenseSeq θ₀ hδ.le) P id S ∂Measure.pi (fun _ : Fin n => P)Proof (Lean source)
theorem scalar_parametric_expected_average_le_of_bounded {X E : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (F : E → X → ℝ) (L : X → ℝ) (hFmeas : ∀ θ, Measurable (F θ)) (hLmeas : Measurable L) (hL : ∀ x, 0 ≤ L x) (hL2 : Integrable (fun x => L x ^ 2) P) (θ₀ : E) {δ : ℝ} (hLip : ∀ θ ∈ Metric.closedBall θ₀ δ, ∀ η ∈ Metric.closedBall θ₀ δ, ∀ z, |F θ z - F η z| ≤ L z * ‖θ - η‖) (hzero : ∀ x, F θ₀ x = 0) {M : ℝ} (hδ : 0 < δ) (hM : 0 ≤ M) (hLM : ∀ x, L x ≤ M) : ∫ S : Fin n → X, uniformDeviation n ((fun θ : Metric.closedBall θ₀ δ => F θ.1) ∘ closedBallDenseSeq θ₀ hδ.le) P id S ∂Measure.pi (fun _ : Fin n => P) ≤ 192 * (finrank ℝ E + 1) * δ * sqrt (∫ x, L x ^ 2 ∂P) / sqrt (n : ℝ) := by classical let B := Metric.closedBall θ₀ δ let FB : B → X → ℝ := fun θ => F θ.1 let θc : B := ⟨θ₀, by change dist θ₀ θ₀ ≤ δ simpa using hδ.le⟩ letI : Nonempty B := ⟨θc⟩ let FD : ℕ → X → ℝ := FB ∘ denseSeq B have hcont : ∀ x, Continuous (fun θ : B => FB θ x) := by intro x apply continuous_iff_continuousAt.2 intro θ rw [Metric.continuousAt_iff] intro ε hε refine ⟨ε / (L x + 1), div_pos hε (by linarith [hL x]), ?_⟩ intro η hη have hb := hLip η.1 η.2 θ.1 θ.2 x have hdist : ‖η.1 - θ.1‖ < ε / (L x + 1) := by change dist (η.1 : E) θ.1 < ε / (L x + 1) at hη simpa [dist_eq_norm] using hη rw [Real.dist_eq] calc |FB η x - FB θ x| ≤ L x * ‖η.1 - θ.1‖ := by simpa [FB] using hb _ ≤ (L x + 1) * ‖η.1 - θ.1‖ := by gcongr linarith _ < (L x + 1) * (ε / (L x + 1)) := mul_lt_mul_of_pos_left hdist (by linarith [hL x]) _ = ε := by have hx : 0 < L x + 1 := by linarith [hL x] field_simp have hFDmeas : ∀ k, Measurable (FD k) := fun k => hFmeas _ have henv : ∀ k x, |FD k x| ≤ δ * M := by intro k x let θ : B := denseSeq B k have hp := θ.2 rw [Metric.mem_closedBall, dist_eq_norm] at hp calc |FD k x| ≤ L x * ‖θ.1 - θ₀‖ := by simpa [FD, FB, θ, hzero] using hLip θ.1 θ.2 θ₀ (Metric.mem_closedBall_self hδ.le) x _ ≤ L x * δ := mul_le_mul_of_nonneg_left hp (hL x) _ ≤ M * δ := mul_le_mul_of_nonneg_right (hLM x) hδ.le _ = δ * M := by ring have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity (μ := P) (f := FD) hn id (fun k => by simpa [Function.comp_def] using hFDmeas k) (mul_nonneg hδ.le hM) henv have hpoint (S : Fin n → X) : empiricalRademacherComplexity n FD S ≤ 96 * (finrank ℝ E + 1) * δ * Concentration.empiricalNorm S L / sqrt (n : ℝ) := by dsimp [FD] rw [← _root_.empiricalRademacherComplexity_eq n hcont S] simpa [FB] using parametric_empiricalRademacher_le hn S F L hL θ₀ hLip hzero hδ have hradInt : Integrable (fun S : Fin n → X => empiricalRademacherComplexity n FD S) (Measure.pi (fun _ : Fin n => P)) := by have hm := Concentration.empiricalRademacherComplexity_measurable_countable FD hFDmeas n apply Integrable.of_bound hm.aestronglyMeasurable (δ * M) filter_upwards with S have hrange := Concentration.empiricalRademacherComplexity_mem_Icc FD (mul_nonneg hδ.le hM) henv n S rw [Real.norm_eq_abs, abs_of_nonneg hrange.1] exact hrange.2 have hrhsInt : Integrable (fun S : Fin n → X => 96 * (finrank ℝ E + 1) * δ * Concentration.empiricalNorm S L / sqrt (n : ℝ)) (Measure.pi (fun _ : Fin n => P)) := by convert (empiricalNorm_integrable P hn L hLmeas hL2).const_mul (96 * (finrank ℝ E + 1) * δ / sqrt (n : ℝ)) using 1 funext S ring have hrad : rademacherComplexity n FD P id ≤ 96 * (finrank ℝ E + 1) * δ * sqrt (∫ x, L x ^ 2 ∂P) / sqrt (n : ℝ) := by rw [Concentration.rademacherComplexity_eq] have hi := integral_mono hradInt hrhsInt hpoint let c : ℝ := 96 * (finrank ℝ E + 1) * δ / sqrt (n : ℝ) have hc : 0 ≤ c := by dsimp [c] positivity have hfun : (fun S : Fin n → X => 96 * (finrank ℝ E + 1) * δ * Concentration.empiricalNorm S L / sqrt (n : ℝ)) = fun S => c * Concentration.empiricalNorm S L := by funext S dsimp [c] ring have hE := expected_empiricalNorm_le P hn L hLmeas hL2 calc _ ≤ ∫ S : Fin n → X, 96 * (finrank ℝ E + 1) * δ * Concentration.empiricalNorm S L / sqrt (n : ℝ) ∂Measure.pi (fun _ : Fin n => P) := by simpa [Function.comp_def] using hi _ = c * ∫ S : Fin n → X, Concentration.empiricalNorm S L ∂Measure.pi (fun _ : Fin n => P) := by rw [hfun, integral_const_mul] _ ≤ c * sqrt (∫ x, L x ^ 2 ∂P) := mul_le_mul_of_nonneg_left hE hc _ = _ := by dsimp [c]; ring have hseq : closedBallDenseSeq θ₀ hδ.le = denseSeq B := by rfl calc _ ≤ 2 • rademacherComplexity n FD P id := by rw [hseq] simpa [FD, FB, B] using hsymm _ ≤ 2 • (96 * (finrank ℝ E + 1) * δ * sqrt (∫ x, L x ^ 2 ∂P) / sqrt (n : ℝ)) := by simpa [nsmul_eq_mul] using mul_le_mul_of_nonneg_left hrad (by norm_num : (0 : ℝ) ≤ 2) _ = _ := by simp [nsmul_eq_mul]; ring -
uniformDeviation_le_add_envelopelemma — The uniform deviation of a class is bounded by the deviation of an approximating class plus empirical and population means of the error envelope under a population law, at positive sample size, on a sample. The main and approximating classes are measurable, the error envelope is integrable, and the approximation obeys boundedness and the pointwise error bound.hypothesesX ι :P :n :ℕhn :0 < nF H :ι → X → ℝT :X → ℝhFmeas :∀ i, Measurable (F i)hHmeas :∀ i, Measurable (H i)hTint :Integrable T PB :ℝhHbound :∀ i x, |H i x| ≤ BhDiff :∀ i x, |F i x - H i x| ≤ T xS :Fin n → XconclusionuniformDeviation n F P id S≤ uniformDeviation n H P id S + ((n : ℝ)⁻¹ * ∑ k : Fin n, T (S k) + ∫ x, T x ∂P)Proof (Lean source)
lemma uniformDeviation_le_add_envelope {X ι : Type*} [MeasurableSpace X] [Nonempty ι] (P : Measure X) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) (F H : ι → X → ℝ) (T : X → ℝ) (hFmeas : ∀ i, Measurable (F i)) (hHmeas : ∀ i, Measurable (H i)) (hTint : Integrable T P) {B : ℝ} (hHbound : ∀ i x, |H i x| ≤ B) (hDiff : ∀ i x, |F i x - H i x| ≤ T x) (S : Fin n → X) : uniformDeviation n F P id S ≤ uniformDeviation n H P id S + ((n : ℝ)⁻¹ * ∑ k : Fin n, T (S k) + ∫ x, T x ∂P) := by have hHint (i : ι) : Integrable (H i) P := Integrable.of_bound (hHmeas i).aestronglyMeasurable B (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hHbound i x) have hDint (i : ι) : Integrable (fun x => F i x - H i x) P := Integrable.mono' hTint (hFmeas i |>.sub (hHmeas i)).aestronglyMeasurable (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hDiff i x) have hFint (i : ι) : Integrable (F i) P := by have hs := (hDint i).add (hHint i) exact hs.congr (ae_of_all _ fun x => by simp) have hbddH : BddAbove (range fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, H i (S k) - ∫ x, H i x ∂P|) := by refine ⟨2 * B, ?_⟩ rintro _ ⟨i, rfl⟩ have havg : |(n : ℝ)⁻¹ * ∑ k : Fin n, H i (S k)| ≤ B := by rw [abs_mul, abs_of_pos (inv_pos.mpr (by exact_mod_cast hn))] calc (n : ℝ)⁻¹ * |∑ k : Fin n, H i (S k)| ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, |H i (S k)| := by gcongr exact Finset.abs_sum_le_sum_abs _ _ _ ≤ (n : ℝ)⁻¹ * ∑ _k : Fin n, B := by gcongr with k exact hHbound i (S k) _ = B := by simp [hn.ne'] have hint : |∫ x, H i x ∂P| ≤ B := by calc |∫ x, H i x ∂P| ≤ ∫ x, |H i x| ∂P := abs_integral_le_integral_abs _ ≤ ∫ _x, B ∂P := integral_mono (hHint i).abs (integrable_const B) (hHbound i) _ = B := by simp exact (abs_sub _ _).trans (by linarith) unfold uniformDeviation simp only [id_eq] refine ciSup_le fun i => ?_ have hcenterDiff : |((n : ℝ)⁻¹ * ∑ k : Fin n, F i (S k) - ∫ x, F i x ∂P) - ((n : ℝ)⁻¹ * ∑ k : Fin n, H i (S k) - ∫ x, H i x ∂P)| ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, T (S k) + ∫ x, T x ∂P := by have hsample : |∑ k : Fin n, (F i (S k) - H i (S k))| ≤ ∑ k : Fin n, T (S k) := (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum fun k _ => hDiff i (S k)) have hint : |∫ x, F i x - H i x ∂P| ≤ ∫ x, T x ∂P := by calc |∫ x, F i x - H i x ∂P| ≤ ∫ x, |F i x - H i x| ∂P := abs_integral_le_integral_abs _ ≤ ∫ x, T x ∂P := integral_mono (hDint i).abs hTint (hDiff i) rw [integral_sub (hFint i) (hHint i)] at hint calc _ = |(n : ℝ)⁻¹ * ∑ k : Fin n, (F i (S k) - H i (S k)) - (∫ x, F i x ∂P - ∫ x, H i x ∂P)| := by rw [Finset.sum_sub_distrib] congr 1 <;> ring _ ≤ |(n : ℝ)⁻¹ * ∑ k : Fin n, (F i (S k) - H i (S k))| + |∫ x, F i x ∂P - ∫ x, H i x ∂P| := abs_sub _ _ _ ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, T (S k) + ∫ x, T x ∂P := by rw [abs_mul, abs_of_pos (inv_pos.mpr (by exact_mod_cast hn))] gcongr let a := (n : ℝ)⁻¹ * ∑ k : Fin n, F i (S k) - ∫ x, F i x ∂P let b := (n : ℝ)⁻¹ * ∑ k : Fin n, H i (S k) - ∫ x, H i x ∂P let e := (n : ℝ)⁻¹ * ∑ k : Fin n, T (S k) + ∫ x, T x ∂P have hab : |a - b| ≤ e := by simpa [a, b, e] using hcenterDiff calc |a| = |b + (a - b)| := by congr 1 <;> ring _ ≤ |b| + |a - b| := abs_add_le _ _ _ ≤ |b| + e := by gcongr _ ≤ (⨆ j, |(n : ℝ)⁻¹ * ∑ k : Fin n, H j (S k) - ∫ x, H j x ∂P|) + e := by gcongr exact le_ciSup hbddH i