Stat.Concentration.Covering.Dudley­Entropy

Dudley's chaining bound.

Chaining 6 core · 12 supporting This file constructs dyadic cover approximations and chain increments in the empirical pseudometric. ★ split_main_and_increment_terms

Finite Dudley chains

This file constructs dyadic cover approximations and chain increments in the empirical pseudometric. It establishes boundedness of the main and increment suprema and splits the signed Rademacher average into the pieces estimated by the later parts of the Dudley argument.

abbrev ej reviewed
Causalean.Stat.Concentration

The dyadic radius at a chaining level is the initial radius divided by two repeatedly at each successive level. These radii set the resolution of the finite covers in the Dudley entropy argument.

Definition (Lean source)
parameters
c :
ℝ
def
ej c :
ℕ → ℝ
given by
fun j ↦ c/(2^j : ℝ)
Causalean.Stat.Concentration.ej · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:66
abbrev cj reviewed
Causalean.Stat.Concentration

At each positive dyadic radius, this selects a finite cover of the empirical function class. The selected cover supplies the approximation candidates at that level of the chaining construction.

Definition (Lean source)
parameters
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
j :
ℕ
def
cj c_pos h j :
Finset (EmpiricalFunctionSpace F S)
given by
coveringFinset h (ej_pos c_pos j)
Causalean.Stat.Concentration.cj · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:79 · uses EmpiricalFunctionSpace , instPseudoMetricSpaceEmpiricalFunctionSpace
abbrev signs_card_inv reviewed
Causalean.Stat.Concentration

For a sample size, the inverse sign-vector count is the reciprocal of the number of possible Rademacher sign vectors of that length. It normalizes the averages over signs in the chaining argument.

Definition (Lean source)
parameters
m :
ℕ
def
signs_card_inv m :
ℝ
given by
(card (Signs m) : ℝ)⁻¹
Causalean.Stat.Concentration.signs_card_inv · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:86
def coverApprox reviewed
Causalean.Stat.Concentration

Each function in the empirical class is assigned one representative from the finite cover at every dyadic resolution. The assigned representative is within that resolution's radius and is used to form the chaining approximation.

Definition (Lean source)
parameters
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
def
coverApprox c_pos h :
ι → ℕ → EmpiricalFunctionSpace F S
given by
fun fh j => choose (exists_cover_approximation c_pos h fh j)
Causalean.Stat.Concentration.coverApprox · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:120 · uses EmpiricalFunctionSpace , instPseudoMetricSpaceEmpiricalFunctionSpace
def chainApprox reviewed
Causalean.Stat.Concentration

The chaining approximation is zero at the coarsest level and otherwise uses the selected finite-cover representative at the corresponding dyadic resolution. It provides the successive approximations whose increments control empirical Rademacher complexity.

Definition (Lean source)
parameters
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
def
chainApprox c_pos h :
ι → ℕ → Z → ℝ
given by
fun fh j => if j = 0 then 0 else (coverApprox c_pos h fh j : Z → ℝ)
Causalean.Stat.Concentration.chainApprox · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:147 · uses EmpiricalFunctionSpace , instPseudoMetricSpaceEmpiricalFunctionSpace
lemma split_main_and_increment_terms reviewed
Causalean.Stat.Concentration

For a function class evaluated on a finite sample, a positive radius and evidence of its positivity, a uniform empirical-radius bound, total boundedness of the empirical class, and a terminal chaining level, the empirical Rademacher complexity is bounded by the sum of the terminal approximation term and all successive chaining increments.

Formal statement
hypotheses
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
0 < c
shared
cs :
∀ f : ι, empiricalNorm S (F f) ≤ c
h :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
n :
ℕ
conclusion
empiricalRademacherComplexity_without_abs m F S
≤ ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh (S i)) - chainApprox c_pos h fh n (S i))))
+ ∑ j : Fin n, ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * (chainApprox c_pos h fh (j + 1) (S i) - chainApprox c_pos h fh j (S i))))
Proof (Lean source)
lemma split_main_and_increment_terms {c_pos : 0 < c} (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) : empiricalRademacherComplexity_without_abs m F S ≤ ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh (S i)) - chainApprox c_pos h fh n (S i)))) + ∑ j : Fin n, ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * (chainApprox c_pos h fh (j + 1) (S i) - chainApprox c_pos h fh j (S i)))) := by by_cases m_pos : m = 0 · simp [m_pos] subst m_pos dsimp [empiricalRademacherComplexity_without_abs] simp · calc _ = signs_card_inv m * ((m : ℝ)⁻¹ * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i)))) := by dsimp [empiricalRademacherComplexity_without_abs, signs_card_inv] apply congrArg rw [Finset.mul_sum] apply congrArg ext σ let H : ι → ℝ := fun i => ∑ k : Fin m, (σ k : ℝ) * F i (S k) change ⨆ i, (↑m)⁻¹ * H i = (↑m)⁻¹ * ⨆ i, H i refine symm (Real.mul_iSup_of_nonneg (by simp) H) _ = (m : ℝ)⁻¹ * (signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i)))) := by ring _ = (m : ℝ)⁻¹ * (signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * (((F fh) (S i) - chainApprox c_pos h fh n (S i)) + (∑ j : Fin n, (chainApprox c_pos h fh ((j : ℕ) + 1) (S i) - chainApprox c_pos h fh ((j : ℕ)) (S i)))))) := by repeat apply congrArg ext σ repeat apply congrArg ext fh apply congrArg ext i apply congrArg symm have h := congrArg (fun (h : Z → ℝ) => h (S i)) (chain_decomposition c_pos h fh n) simp only [Pi.add_apply, Pi.sub_apply, Finset.sum_apply] at h symm exact h _ ≤ (m : ℝ)⁻¹ * ((signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i) - chainApprox c_pos h fh n (S i)))) + signs_card_inv m * ∑ j : Fin n, (∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * (chainApprox c_pos h fh (j + 1) (S i) - chainApprox c_pos h fh j (S i))))) := by rw [<- left_distrib] rw [Finset.sum_comm] apply mul_le_mul_of_nonneg_left · apply mul_le_mul_of_nonneg_left · have w : (∑ σ : Signs m, ⨆ fh, ∑ i, (σ i : ℝ) * (F fh (S i) - chainApprox c_pos h fh n (S i))) + ∑ y : Signs m, ∑ x : Fin n, ⨆ fh, ∑ i, (y i : ℝ) * (chainApprox c_pos h fh (↑x + 1) (S i) - chainApprox c_pos h fh (↑x) (S i)) = ∑ σ : Signs m, ((⨆ fh, ∑ i, (σ i : ℝ) * (F fh (S i) - chainApprox c_pos h fh n (S i))) + (∑ x : Fin n, ⨆ fh, ∑ i, (σ i : ℝ) * (chainApprox c_pos h fh (↑x + 1) (S i) - chainApprox c_pos h fh (↑x) (S i)))) := by let chainApprox_increment_bound (σ : Signs m) := ⨆ fh, ∑ i, (σ i : ℝ) * (F fh (S i) - chainApprox c_pos h fh n (S i)) let chainApprox_pointwise_bound (y : Signs m) := ∑ x : Fin n, ⨆ fh, ∑ i, (y i : ℝ) * (chainApprox c_pos h fh (↑x + 1) (S i) - chainApprox c_pos h fh (↑x) (S i)) have w' : ∑ σ : Signs m, chainApprox_increment_bound σ + ∑ y : Signs m, chainApprox_pointwise_bound y = ∑ σ : Signs m, (chainApprox_increment_bound σ + chainApprox_pointwise_bound σ) := symm Finset.sum_add_distrib dsimp [chainApprox_increment_bound, chainApprox_pointwise_bound] at w' exact w' rw [w] apply Finset.sum_le_sum intro i hi have q : ⨆ fh, ∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1) + ∑ j : Fin n, (chainApprox c_pos h fh ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h fh ((j : ℕ)) (S i_1))) ≤ (⨆ fh, ∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) + ⨆ fh, ∑ x : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h fh (↑x + 1) (S i_1) - chainApprox c_pos h fh (↑x) (S i_1)) := by apply ciSup_le intro x -- split the inner sum into a constant part and the telescoping part have hx_split : (∑ i_1, (i i_1 : ℝ) * (F x (S i_1) - chainApprox c_pos h x n (S i_1) + ∑ j : Fin n, (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)))) = (∑ i_1, (i i_1 : ℝ) * (F x (S i_1) - chainApprox c_pos h x n (S i_1))) + (∑ i_1, (i i_1 : ℝ) * (∑ j : Fin n, (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)))) := by -- distribute the product over the inner addition and split the outer sum simp [mul_add, Finset.sum_add_distrib] -- bound each part by the respective suprema have hx1 : (∑ i_1, (i i_1 : ℝ) * (F x (S i_1) - chainApprox c_pos h x n (S i_1))) ≤ ⨆ fh, ∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1)) := by apply le_ciSup_of_le · exact splitBound.bddAbove_main_term cs h n m_pos i · exact Preorder.le_refl (∑ i_1, ↑↑(i i_1) * (F x (S i_1) - chainApprox c_pos h x n (S i_1))) calc (∑ i_1, (i i_1 : ℝ) * (F x (S i_1) - chainApprox c_pos h x n (S i_1) + ∑ j : Fin n, (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)))) = _ := hx_split _ ≤ (⨆ fh, ∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) + (∑ i_1, (i i_1 : ℝ) * (∑ j : Fin n, (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)))) := by nlinarith _ ≤ (⨆ fh, ∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) + (⨆ fh, ∑ x : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h fh (↑x + 1) (S i_1) - chainApprox c_pos h fh (↑x) (S i_1))) := by -- rewrite the second sum as a double sum and take fh = x in the supremum have hx2_swap : (∑ i_1, (i i_1 : ℝ) * (∑ j : Fin n, (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)))) = ∑ j : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)) := by -- expand the outer product into an inner sum and then swap the summations have h_expand : (∑ i_1, (i i_1 : ℝ) * (∑ j : Fin n, (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)))) = ∑ i_1, ∑ j : Fin n, (i i_1 : ℝ) * (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1)) := by apply Finset.sum_congr rfl intro i1 hi1 -- move the scalar inside the inner sum rw [Finset.mul_sum] rw [h_expand] rw [Finset.sum_comm] have hx2 : (∑ j : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h x ((j : ℕ) + 1) (S i_1) - chainApprox c_pos h x ((j : ℕ)) (S i_1))) ≤ ⨆ fh, ∑ x_1 : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1)) := by apply le_ciSup_of_le · exact splitBound.bddAbove_increment_term cs h n m_pos i · apply Preorder.le_refl -- combine both bounds rw [hx2_swap] apply add_le_add_right exact hx2 apply le_trans q rw [add_le_add_iff_left] apply ciSup_le intro x' apply Finset.sum_le_sum intro i_1 hi_1 apply le_ciSup_of_le · rw [bddAbove_def] use m * (2 * (√↑m * c)) simp intro a calc _ ≤ ∑ i_2, |(i i_2 : ℝ) * (chainApprox c_pos h a (↑i_1 + 1) (S i_2) - chainApprox c_pos h a (↑i_1) (S i_2))| := Finset.sum_le_sum (fun i_2 hi_2 ↦ le_abs_self ((i i_2 : ℝ) * (chainApprox c_pos h a (↑i_1 + 1) (S i_2) - chainApprox c_pos h a (↑i_1) (S i_2)))) _ ≤ ∑ i_2 : Fin m, 2 * (√↑m * c) := by apply Finset.sum_le_sum intro i_2 hi_2 rw [abs_mul] simp apply chainApprox_increment_bound · apply Nat.pos_of_ne_zero m_pos · exact cs _ = _ := by simp · change ∑ i_1_1, (i i_1_1 : ℝ) * (chainApprox c_pos h x' (↑i_1 + 1) (S i_1_1) - chainApprox c_pos h x' (↑i_1) (S i_1_1)) ≤ ∑ i_2, (i i_2 : ℝ) * (chainApprox c_pos h x' (↑i_1 + 1) (S i_2) - chainApprox c_pos h x' (↑i_1) (S i_2)) simp · dsimp [signs_card_inv] simp · simp _ = (m : ℝ)⁻¹ * ((signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i) - chainApprox c_pos h fh n (S i)))) + ∑ j : Fin n, ( signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * (chainApprox c_pos h fh (j + 1) (S i) - chainApprox c_pos h fh j (S i))))) := by simp left simp [Finset.mul_sum] _ = ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i) - chainApprox c_pos h fh n (S i)))) + (m : ℝ)⁻¹ * ∑ j : Fin n, ( signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * (chainApprox c_pos h fh (j + 1) (S i) - chainApprox c_pos h fh j (S i)))) := by rw [mul_add] rw [mul_assoc] _ = _ := by simp only [add_right_inj] simp [Finset.mul_sum, mul_assoc]
Causalean.Stat.Concentration.split_main_and_increment_terms · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:361 · uses EmpiricalFunctionSpace , chainApprox , empiricalNorm , instPseudoMetricSpaceEmpiricalFunctionSpace , signs_card_inv
12 supporting declarations (lemmas, instances)
  • term_le_total_sum_of_nonneg theorem — A nonnegative term in a finite sum is bounded by the full sum of nonnegative terms.
    hypotheses
    α :
    Type u
    Fintype α
    M :
    Type*
    AddCommMonoid M
    Preorder M
    IsOrderedAddMonoid M
    j :
    α
    f :
    α → M
    h0 :
    ∀ j, 0 ≤ f j
    conclusion
    f j ≤ ∑ i : α, f i
    Proof (Lean source)
    theorem term_le_total_sum_of_nonneg {α : Type u} [Fintype α] {M : Type*} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] (j : α) (f : α → M) (h0 : ∀ j, 0 ≤ f j) : f j ≤ ∑ i : α, f i := by classical have hj : j ∈ (Finset.univ : Finset α) := by simp have hsum : (Finset.univ.erase j).sum (fun i : α => f i) + f j = ∑ i : α, f i := by exact Finset.sum_erase_add _ _ hj have h_nonneg : 0 ≤ (Finset.univ.erase j).sum (fun i : α => f i) := by refine Finset.sum_nonneg ?_ intro i hi exact h0 i have h_le : f j ≤ (Finset.univ.erase j).sum (fun i : α => f i) + f j := by simpa [add_comm] using add_le_add_left h_nonneg (f j) exact h_le.trans_eq hsum
    Causalean.Stat.Concentration.term_le_total_sum_of_nonneg · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:41
  • ej_pos lemma — When the initial radius is positive, every dyadic chaining radius is positive.
    hypotheses
    c :
    ℝ
    shared
    c_pos :
    0 < c
    j :
    conclusion
    ej c j > 0
    Proof (Lean source)
    lemma ej_pos (c_pos : 0 < c) : ∀ j, (ej c j > 0) := by intro j dsimp [ej] simp only [gt_iff_lt, Nat.ofNat_pos, pow_pos, div_pos_iff_of_pos_right] exact c_pos
    Causalean.Stat.Concentration.ej_pos · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:71
  • ej_nonneg lemma — When the initial radius is positive, every dyadic chaining radius is nonnegative.
    hypotheses
    c :
    ℝ
    shared
    c_pos :
    0 < c
    j :
    conclusion
    0 ≤ ej c j
    Proof (Lean source)
    lemma ej_nonneg (c_pos : 0 < c) : ∀ j, (0 ≤ ej c j) := fun j ↦ le_of_lt (ej_pos c_pos j)
    Causalean.Stat.Concentration.ej_nonneg · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:91
  • e_nonempty lemma — The empirical function space of a nonempty indexed class is nonempty.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    conclusion
    (Set.univ : Set (EmpiricalFunctionSpace F S)).Nonempty
    Proof (Lean source)
    lemma e_nonempty : (Set.univ : Set (EmpiricalFunctionSpace F S)).Nonempty := by classical obtain ⟨i⟩ := (inferInstance : Nonempty ι) exact ⟨⟨i⟩, by simp⟩
    Causalean.Stat.Concentration.e_nonempty · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:95
  • exists_cover_approximation lemma — For a positive initial radius and a totally bounded empirical function space, every indexed function has a representative in each finite dyadic cover within that cover's radius.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    shared
    c_pos :
    0 < c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    fh :
    ι
    j :
    ℕ
    conclusion
    ∃ f_j : EmpiricalFunctionSpace F S,
    conclusion 1
    f_j ∈ cj c_pos h j
    conclusion 2
    empiricalDist S (F fh) f_j ≤ ej c j
    Proof (Lean source)
    lemma exists_cover_approximation (c_pos : 0 < c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (fh : ι) (j : ℕ) : ∃ f_j : EmpiricalFunctionSpace F S, f_j ∈ cj c_pos h j ∧ empiricalDist S (F fh) f_j ≤ ej c j := by have : ⟨fh⟩ ∈ ⋃ y ∈ coveringFinset h (ej_pos c_pos j), ball y (ej c j) := coveringFinset_cover h (ej_pos c_pos j) (Set.mem_univ fh) obtain ⟨y, hy⟩ := Set.mem_iUnion.mp this obtain ⟨hy', hy''⟩ := Set.mem_iUnion.mp hy use ⟨y.index⟩ constructor · exact hy' · exact le_of_lt hy''
    Causalean.Stat.Concentration.exists_cover_approximation · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:103
  • coverApprox_mem_cover lemma — For a positive initial radius and a totally bounded empirical function space, the chosen approximation belongs to its finite dyadic cover.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    shared
    c_pos :
    0 < c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    fh :
    ι
    j :
    ℕ
    conclusion
    coverApprox c_pos h fh j ∈ cj c_pos h j
    Proof (Lean source)
    lemma coverApprox_mem_cover (c_pos : 0 < c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (fh : ι) (j : ℕ) : coverApprox c_pos h fh j ∈ cj c_pos h j := by classical exact (Classical.choose_spec (exists_cover_approximation c_pos h fh j)).1
    Causalean.Stat.Concentration.coverApprox_mem_cover · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:129
  • empiricalDist_coverApprox_le_radius lemma — For a positive initial radius and a totally bounded empirical function space, the empirical distance from a function to its chosen cover representative is at most the dyadic radius.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    shared
    c_pos :
    0 < c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    fh :
    ι
    j :
    ℕ
    conclusion
    empiricalDist S (F fh) (coverApprox c_pos h fh j) ≤ ej c j
    Proof (Lean source)
    lemma empiricalDist_coverApprox_le_radius (c_pos : 0 < c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (fh : ι) (j : ℕ) : empiricalDist S (F fh) (coverApprox c_pos h fh j) ≤ ej c j := by classical exact (Classical.choose_spec (exists_cover_approximation c_pos h fh j)).2
    Causalean.Stat.Concentration.empiricalDist_coverApprox_le_radius · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:138
  • chainApprox_def lemma — For a positive initial radius and a totally bounded empirical function space, the level-zero chain approximation is zero and every other level is the chosen cover approximation.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    shared
    c_pos :
    0 < c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    fh j :
    conclusion
    chainApprox c_pos h fh j = if j = 0 then 0 else (coverApprox c_pos h fh j : Z → ℝ)
    Proof (Lean source)
    lemma chainApprox_def (c_pos : 0 < c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) : ∀ fh j, chainApprox c_pos h fh j = if j = 0 then 0 else (coverApprox c_pos h fh j : Z → ℝ) := by intro fh j dsimp [chainApprox]
    Causalean.Stat.Concentration.chainApprox_def · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:156
  • chainApprox_succ lemma — For a positive initial radius and a totally bounded empirical function space, the chain approximation at every positive level equals the chosen cover approximation at that level.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    shared
    c_pos :
    0 < c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    fh :
    ι
    j :
    ℕ
    conclusion
    chainApprox c_pos h fh (j + 1) = (coverApprox c_pos h fh (j + 1) : Z → ℝ)
    Proof (Lean source)
    lemma chainApprox_succ (c_pos : 0 < c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (fh : ι) (j : ℕ) : chainApprox c_pos h fh (j + 1) = (coverApprox c_pos h fh (j + 1) : Z → ℝ) := by simp [chainApprox]
    Causalean.Stat.Concentration.chainApprox_succ · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:168
  • pointwise_bound_from_empirical_norm lemma — If every function has empirical norm at most a given bound on a positive-size sample, then its absolute value at each sampled observation is at most the sample-size square root times that bound.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    shared
    cs :
    ∀ f : ι, empiricalNorm S (F f) ≤ c
    i :
    Fin m
    hm_pos :
    0 < m
    f :
    ι
    conclusion
    |F f (S i)| ≤ √↑m * c
    Proof (Lean source)
    lemma pointwise_bound_from_empirical_norm (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) (i : Fin m) (hm_pos : 0 < m) : ∀ (f : ι), |F f (S i)| ≤ √↑m * c := by intro f dsimp [empiricalNorm] at cs have fcs := cs f -- from a finite-sample ℓ₂ bound to a pointwise bound via the coordinate projection inequality have hm_pos : 0 < (m : ℝ) := by norm_cast have hm_sqrt_pos : 0 < sqrt (m : ℝ) := Real.sqrt_pos.2 hm_pos have hproj := empiricalDist_proj (S := S) (f := F f) (i := i) have hcancel : sqrt (m : ℝ) ≠ 0 := ne_of_gt hm_sqrt_pos have h1 : |F f (S i)| ≤ √↑m * empiricalNorm S (F f) := by have hproj' := mul_le_mul_of_nonneg_left hproj (le_of_lt hm_sqrt_pos) -- simplify the left side using positivity of √m have hleft : √↑m * (|F f (S i)| / √↑m) = |F f (S i)| := by field_simp [hcancel] simpa [hleft] using hproj' calc |F f (S i)| ≤ √↑m * empiricalNorm S (F f) := h1 _ ≤ √↑m * c := by apply mul_le_mul_of_nonneg_left fcs exact le_of_lt hm_sqrt_pos
    Causalean.Stat.Concentration.pointwise_bound_from_empirical_norm · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:195
  • bddAbove_main_term theorem — The main remainder term in the Dudley chain has a finite upper bound.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    0 < c
    shared
    cs :
    ∀ (f : ι), empiricalNorm S (F f) ≤ c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    n :
    ℕ
    m_pos :
    ¬m = 0
    i :
    Signs m
    conclusion
    BddAbove (range fun fh ↦ ∑ i_1, ↑↑(i i_1) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1)))
    Proof (Lean source)
    theorem splitBound.bddAbove_main_term {c_pos : 0 < c} (cs : ∀ (f : ι), empiricalNorm S (F f) ≤ c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : ¬m = 0) (i : Signs m) : BddAbove (range fun fh ↦ ∑ i_1, ↑↑(i i_1) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) := by rw [bddAbove_def] classical refine ⟨m * (2 * (sqrt (m : ℝ) * c)), ?_⟩ intro y hy rcases hy with ⟨fh, rfl⟩ have hmpos : 0 < m := Nat.pos_of_ne_zero m_pos calc (∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) ≤ ∑ i_1, |(i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))| := by refine Finset.sum_le_sum ?_ intro _ _ exact le_abs_self _ _ = ∑ i_1, |F fh (S i_1) - chainApprox c_pos h fh n (S i_1)| := by apply Finset.sum_congr rfl intro _ _ simp [abs_mul] _ ≤ ∑ i_1, (|F fh (S i_1)| + |chainApprox c_pos h fh n (S i_1)|) := by refine Finset.sum_le_sum ?_ intro i_1 _ have htri : |F fh (S i_1) - chainApprox c_pos h fh n (S i_1)| ≤ |F fh (S i_1)| + |chainApprox c_pos h fh n (S i_1)| := by exact abs_sub (F fh (S i_1)) (chainApprox c_pos h fh n (S i_1)) exact htri _ ≤ ∑ i_1, (sqrt (m : ℝ) * c + sqrt (m : ℝ) * c) := by refine Finset.sum_le_sum ?_ intro i_1 _ have hF : |F fh (S i_1)| ≤ sqrt (m : ℝ) * c := pointwise_bound_from_empirical_norm cs i_1 hmpos fh have hG : |chainApprox c_pos h fh n (S i_1)| ≤ sqrt (m : ℝ) * c := chainApprox_pointwise_bound c_pos hmpos cs n h i_1 fh have : |F fh (S i_1)| + |chainApprox c_pos h fh n (S i_1)| ≤ sqrt (m : ℝ) * c + sqrt (m : ℝ) * c := by nlinarith exact this _ = m * (2 * (sqrt (m : ℝ) * c)) := by simp grind
    Causalean.Stat.Concentration.splitBound.bddAbove_main_term · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:253
  • bddAbove_increment_term theorem — The sum of chaining increment terms has a finite upper bound.
    hypotheses
    Z :
    Type v
    shared
    m :
    ℕ
    shared
    ι :
    Type u
    ι → Z → ℝ
    shared
    S :
    Fin m → Z
    shared
    c :
    ℝ
    0 < c
    shared
    cs :
    ∀ (f : ι), empiricalNorm S (F f) ≤ c
    h :
    TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
    n :
    ℕ
    m_pos :
    ¬m = 0
    i :
    Signs m
    conclusion
    BddAbove (Set.range fun fh ↦ ∑ x_1 : Fin n, ∑ i_1, ↑↑(i i_1) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1)))
    Proof (Lean source)
    theorem splitBound.bddAbove_increment_term {c_pos : 0 < c} (cs : ∀ (f : ι), empiricalNorm S (F f) ≤ c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : ¬m = 0) (i : Signs m) : BddAbove (Set.range fun fh ↦ ∑ x_1 : Fin n, ∑ i_1, ↑↑(i i_1) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1))) := by rw [bddAbove_def] classical refine ⟨(n : ℝ) * m * (2 * (sqrt (m : ℝ) * c)), ?_⟩ intro y hy rcases hy with ⟨fh, rfl⟩ have hmpos : 0 < m := Nat.pos_of_ne_zero m_pos calc (∑ x_1 : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1))) ≤ ∑ x_1 : Fin n, ∑ i_1, |(i i_1 : ℝ) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1))| := by refine Finset.sum_le_sum ?_ intro _ _ refine Finset.sum_le_sum ?_ intro _ _ exact le_abs_self _ _ = ∑ x_1 : Fin n, ∑ i_1, |chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1)| := by apply Finset.sum_congr rfl intro _ _ apply Finset.sum_congr rfl intro i_1 _ obtain ⟨v, hv⟩ := i i_1 simp at hv cases hv with | inl hv => simp [hv]; rw [<- abs_neg]; apply congrArg; linarith | inr hv => simp [hv] _ ≤ ∑ x_1 : Fin n, ∑ i_1, 2 * (sqrt (m : ℝ) * c) := by refine Finset.sum_le_sum ?_ intro x_1 _ refine Finset.sum_le_sum ?_ intro i_1 _ have hdiff : |chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1)| ≤ 2 * (sqrt (m : ℝ) * c) := chainApprox_increment_bound c_pos hmpos cs (↑x_1) h i_1 fh nlinarith _ = (n : ℝ) * m * (2 * (sqrt (m : ℝ) * c)) := by simp [Finset.sum_const, Finset.card_univ, mul_assoc, mul_left_comm, mul_comm]
    Causalean.Stat.Concentration.splitBound.bddAbove_increment_term · Causalean/Stat/Concentration/Covering/DudleyEntropy/Chaining.lean:302
Entropy­Bound 1 core · 0 supporting This file assembles the finite-chain and Riemann-integral estimates into dudley_entropy_integral_bound, the signed empirical Rademacher bound for a totally bounded function class at a positive truncation scale. ★ dudley_entropy_integral_bound

Dudley entropy-integral bound

This file assembles the finite-chain and Riemann-integral estimates into dudley_entropy_integral_bound, the signed empirical Rademacher bound for a totally bounded function class at a positive truncation scale.

theorem dudley_entropy_integral_bound reviewed
Causalean.Stat.Concentration

Dudley entropy-integral bound, without the outer absolute value. Fix a positive scale ε that is strictly less than half the common empirical-norm envelope c, where the sample size m is positive, every member of the class has empirical norm on the sample at most c, and the sample-restricted function class is totally bounded in the empirical pseudometric. Then the empirical Rademacher complexity computed without the outer absolute value is at most 4ε + (12/√m) ∫_ε^(c/2) √(log(coveringNumber' x)) dx, the usual Dudley chaining bound in terms of the covering-number entropy integral.

Formal statement
hypotheses
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
ε :
ℝ
ε_pos :
0 < ε
h' :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
m_pos :
0 < m
cs :
∀ f : ι, empiricalNorm S (F f) ≤ c
ε_le_c_div_2 :
ε < c/2
conclusion
empiricalRademacherComplexity_without_abs m F S
≤ (4 * ε + (12 / (sqrt m)) * (∫ (x : ℝ) in ε..(c/2),√(log (coveringNumber' h' x))))
Proof (Lean source)
theorem dudley_entropy_integral_bound {ε : ℝ} (ε_pos : 0 < ε) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (m_pos : 0 < m) (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) (ε_le_c_div_2 : ε < c/2) : empiricalRademacherComplexity_without_abs m F S ≤ (4 * ε + (12 / (sqrt m)) * (∫ (x : ℝ) in ε..(c/2),√(log (coveringNumber' h' x)))) := by obtain ⟨n, ⟨nw1, nw2⟩⟩ := choose_dyadic_scale_for_epsilon ε ε_pos ε_le_c_div_2 have ε_c : ε ≤ c := by linarith have c_pos : 0 < c := lt_of_le_of_lt' ε_c ε_pos apply le_trans (entropy_sum_to_integral_bound c_pos h' n m_pos cs) apply add_le_add · linarith · apply mul_le_mul_of_nonneg_left · apply intervalIntegral.integral_mono_interval (le_of_lt nw1) · dsimp [ej] rw [div_le_div_iff_of_pos_left] · have := Nat.one_lt_two_pow' n rw [<- Nat.add_one_le_iff] at this simp only [Nat.reduceAdd] at this norm_cast · exact c_pos · simp · simp · simp · filter_upwards intro a simp · apply AntitoneOn.intervalIntegrable have f0 : Monotone (fun x ↦ √x) := by apply Real.sqrt_le_sqrt apply Monotone.comp_antitoneOn f0 refine antitoneOn_iff_forall_lt.mpr ?_ intro a ha b hb hab dsimp [uIcc] at ha dsimp [Icc] at ha have : min ε (c / 2) = ε := by simp linarith rw [this] at ha dsimp [uIcc] at hb dsimp [Icc] at hb rw [this] at hb apply Real.log_le_log · apply Nat.cast_pos.mpr apply coveringNumber'_nonzero · exact e_nonempty linarith · norm_cast apply coveringNumber'_antitone · simp linarith · simp linarith · exact le_of_lt hab · refine div_nonneg ?_ ?_ · simp · norm_cast simp
Causalean.Stat.Concentration.dudley_entropy_integral_bound · Causalean/Stat/Concentration/Covering/DudleyEntropy/EntropyBound.lean:27 · uses EmpiricalFunctionSpace , coveringNumber' , empiricalNorm , instPseudoMetricSpaceEmpiricalFunctionSpace
Part­A 1 core · 2 supporting This file bounds the first, coarse-scale part of the dyadic Dudley chain. ★ partA_sup_bound

Dudley chaining: coarse-scale term

This file bounds the first, coarse-scale part of the dyadic Dudley chain. It relates the signed empirical sum to empirical distance and proves partA_sup_bound, leaving increment entropy and integral comparison to the subsequent files.

lemma partA_sup_bound reviewed
Causalean.Stat.Concentration

For a function class evaluated on a finite sample, a positive empirical radius, positivity of that radius, total boundedness of the empirical class, a uniform empirical-radius bound, a chaining level, a sign vector, and a selected function, the signed terminal approximation error is at most the sample size times the dyadic radius at that level.

Formal statement
hypotheses
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
cs :
∀ f : ι, empiricalNorm S (F f) ≤ c
n :
ℕ
σ :
Signs m
fh :
ι
conclusion
(∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i) - chainApprox c_pos h fh n (S i)))
≤ (m : ℝ) * (ej c n)
Proof (Lean source)
lemma partA_sup_bound (c_pos : 0 < c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) (n : ℕ) : ∀ (σ : Signs m) (fh : ι), ((∑ i : Fin m, (σ i : ℝ) * ((F fh) (S i) - chainApprox c_pos h fh n (S i))) ≤ (m : ℝ) * (ej c n)) := by intro σ fh unfold ej apply le_trans (signed_sum_le_empiricalDist (F fh) (chainApprox c_pos h fh n) σ) apply mul_le_mul_of_nonneg_left _ (by simp) exact empiricalDist_to_chainApprox_le_ej c_pos h fh n cs
Causalean.Stat.Concentration.partA_sup_bound · Causalean/Stat/Concentration/Covering/DudleyEntropy/PartA.lean:85 · uses EmpiricalFunctionSpace , chainApprox , ej , empiricalNorm , instPseudoMetricSpaceEmpiricalFunctionSpace
2 supporting declarations (lemmas, instances)
Part­B 1 core · 0 supporting The Part B chaining estimate bounds the signed empirical increment sum by dyadic radius decrements weighted by logarithmic covering complexity. ★ partB_bound

The Part B chaining estimate bounds the signed empirical increment sum by dyadic radius decrements weighted by logarithmic covering complexity.

The finite-class construction and clean Massart reduction live in PartBCore; this module exposes the resulting chaining bound.

lemma partB_bound reviewed
Causalean.Stat.Concentration

For a function class evaluated on a finite sample, a positive empirical radius, positivity of that radius, total boundedness of the empirical class, a terminal chaining level, positive sample size, and a uniform empirical-radius bound, the sum of expected signed chaining increments is bounded by the corresponding sum of dyadic radius decrements times logarithmic covering complexities.

Formal statement
hypotheses
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h' :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
n :
ℕ
m_pos :
0 < m
cs :
∀ f : ι, empiricalNorm S (F f) ≤ c
conclusion
∑ j : Fin n, ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((chainApprox c_pos h' fh (j + 1) - chainApprox c_pos h' fh j) (S i))))
≤ ∑ j : Fin n, 6 * (ej c (j + 1) - ej c (j + 2)) * (√(4 * log (coveringNumber' h' (ej c (j + 1)))) / ((sqrt m)))
Proof (Lean source)
lemma partB_bound (c_pos : 0 < c) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : 0 < m) (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) : ∑ j : Fin n, ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((chainApprox c_pos h' fh (j + 1) - chainApprox c_pos h' fh j) (S i)))) ≤ ∑ j : Fin n, 6 * (ej c (j + 1) - ej c (j + 2)) * (√(4 * log (coveringNumber' h' (ej c (j + 1)))) / ((sqrt m))) := by calc _ ≤ ∑ j : Fin n, (sup' (incrementPairFinset c_pos h' n j) (incrementPairFinset_nonempty c_pos h' n j) fun hk ↦ √(∑ i : Fin m, ((hk.1 - hk.2) (S i)) ^ 2)) * (√(2 * log (coveringNumber' h' (ej c (j + 1)) * coveringNumber' h' (ej c j)))) / ↑m := by by_cases n_pos : 0 < n · exact partB_sum_bound_via_massart c_pos h' n m_pos cs n_pos · simp at n_pos rw [n_pos] simp _ = ∑ j : Fin n, (sup' (incrementPairFinset c_pos h' n j) (incrementPairFinset_nonempty c_pos h' n j) fun hk ↦ (√(∑ i : Fin m, ((hk.1 - hk.2) (S i)) ^ 2)) / ↑m) * (√(2 * log (coveringNumber' h' (ej c (j + 1)) * coveringNumber' h' (ej c j)))) := by apply congrArg ext j rw [<- div_mul_eq_mul_div] rw [Mathlib.Tactic.LinearCombination.mul_eq_const] rw [Finset.sup'_div₀] exact Nat.cast_nonneg m _ ≤ ∑ j : Fin n, ((6 * (ej c (j + 1) - ej c (j + 2)) / sqrt m) * (√(2 * log ((coveringNumber' h' (ej c (j + 1))) * (coveringNumber' h' (ej c j)))))) := by refine Finset.sum_le_sum ?_ intro j hj apply mul_le_mul_of_nonneg_right -- The remaining estimate follows from the pair-class representation. · have r0 (hk : (Z → ℝ) × (Z → ℝ)) (hk0 : hk ∈ incrementPairFinset c_pos h' n j) : ∃ fh, (chainApprox c_pos h' fh (j + 1), chainApprox c_pos h' fh j) = hk := by dsimp [incrementPairFinset] at hk0 simp at hk0 dsimp [incrementPairSet] at hk0 exact hk0 have fh (hk : (Z → ℝ) × (Z → ℝ)) (hk0 : hk ∈ incrementPairFinset c_pos h' n j) : ι := choose (r0 hk hk0) suffices ∀ (hk : (Z → ℝ) × (Z → ℝ)) (hk0 : hk ∈ incrementPairFinset c_pos h' n j), (√(∑ i, ((hk.1 - hk.2) (S i)) ^ 2)) / ↑m ≤ 6 * (ej c ((j : ℕ) + 1) - ej c ((j : ℕ) + 2)) / sqrt m from by rw [Finset.sup'_le_iff] exact this intro hk hk0 have hk1 : hk ∈ incrementPairSet c_pos h' n j := by dsimp [incrementPairFinset] at hk0 simp at hk0 exact hk0 dsimp [incrementPairSet] at hk1 obtain ⟨x, fhx⟩ := hk1 have r : √(∑ i, ((hk.1 - hk.2) (S i)) ^ 2) ≤ √(∑ i, ((hk.1 - (F x)) (S i)) ^ 2) + √(∑ i, ((hk.2 - (F x)) (S i)) ^ 2) := by let ai : EuclideanSpace ℝ (Fin m) := toLp 2 fun i ↦ (hk.1 - (F x)) (S i) let aj : EuclideanSpace ℝ (Fin m) := toLp 2 fun i ↦ (hk.2 - (F x)) (S i) have norm_calc : ‖ai - aj‖ = √(∑ i : Fin m, ((hk.1 - hk.2) (S i)) ^ 2) := by calc _ = √(∑ j : Fin m, ‖ai j - aj j‖ ^ 2) := by exact (EuclideanSpace.norm_eq (ai - aj)) _ = _ := by dsimp [ai, aj]; simp calc _ = ‖ai - aj‖ := by dsimp [ai, aj, norm] simp rw [Real.sqrt_eq_rpow];simp _ = ‖ai + (-aj)‖ := rfl _ ≤ ‖ai‖ + ‖(-aj)‖ := norm_add_le ai (-aj) _ = ‖ai‖ + ‖aj‖ := by simp _ = _ := by apply Mathlib.Tactic.LinearCombination.add_eq_eq · dsimp [ai, norm] simp rw [Real.sqrt_eq_rpow];simp · dsimp [aj, norm] simp rw [Real.sqrt_eq_rpow];simp have r' : √(∑ i, ((hk.1 - hk.2) (S i)) ^ 2) / ↑m ≤ √(∑ i, ((hk.1 - (F x)) (S i)) ^ 2) / ↑m + √(∑ i, ((hk.2 - (F x)) (S i)) ^ 2) / ↑m := by have : (√(∑ i, ((hk.1 - (F x)) (S i)) ^ 2) + √(∑ i, ((hk.2 - (F x)) (S i)) ^ 2)) / ↑m = √(∑ i, ((hk.1 - (F x)) (S i)) ^ 2) / ↑m + √(∑ i, ((hk.2 - (F x)) (S i)) ^ 2) / ↑m := by ring rw [← this] exact div_le_div_of_nonneg_right r (Nat.cast_nonneg m) apply le_trans r' have rp : 6 * (ej c ((j : ℕ) + 1) - ej c ((j : ℕ) + 2)) / sqrt m = (ej c (j + 1) / sqrt m) + (ej c j / sqrt m) := by suffices 6 * (ej c ((j : ℕ) + 1) - ej c ((j : ℕ) + 2)) = ej c (j + 1) + ej c j from by rw [this] exact add_div (ej c ((j : ℕ) + 1)) (ej c (j : ℕ)) (sqrt m) have t (j : ℕ) : 2 * ej c ((j : ℕ) + 1) = ej c (j : ℕ) := by have two_ne_zero' : (2 : ℝ) ≠ 0 := two_ne_zero calc 2 * ej c ((j : ℕ) + 1) = 2 * (c / (2 ^ ((j : ℕ) + 1) : ℝ)) := by rfl _ = 2 * (c / ((2 ^ (j : ℕ) : ℝ) * 2)) := by simp [pow_succ] _ = (2 * c) / ((2 ^ (j : ℕ) : ℝ) * 2) := by simpa [mul_comm, mul_left_comm, mul_assoc] using (mul_div_assoc (2 : ℝ) c ((2 ^ (j : ℕ) : ℝ) * 2)).symm _ = (c * 2) / ((2 ^ (j : ℕ) : ℝ) * 2) := by simp [mul_comm] _ = c / (2 ^ (j : ℕ) : ℝ) := mul_div_mul_right c (2 ^ j) two_ne_zero' _ = ej c (j : ℕ) := by simp [ej] calc _ = 6 * ej c ((j : ℕ) + 1) - 6 * ej c ((j : ℕ) + 2) := by simp [mul_sub] _ = 6 * ej c ((j : ℕ) + 1) - 3 * ej c ((j : ℕ) + 1) := by have ht : 6 * ej c ((j : ℕ) + 2) = 3 * ej c ((j : ℕ) + 1) := by have h := t ((j : ℕ) + 1) have h' : 2 * ej c ((j : ℕ) + 2) = ej c ((j : ℕ) + 1) := by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm, add_assoc] using h have h'' := congrArg (fun x : ℝ => (3 : ℝ) * x) h' calc 6 * ej c ((j : ℕ) + 2) = 3 * (2 * ej c ((j : ℕ) + 2)) := by ring _ = 3 * ej c ((j : ℕ) + 1) := by simpa using h'' simp [ht] -- Equivalent dyadic-expression rewrite used in the integral comparison step. _ = 3 * ej c ((j : ℕ) + 1) := by linarith _ = ej c ((j : ℕ) + 1) + 2 * ej c ((j : ℕ) + 1) := by linarith _ = _ := by refine add_left_cancel_iff.mpr ?_ rw [t] have r0 : √(∑ i, ((hk.1 - (F x)) (S i)) ^ 2) / ↑m ≤ ej c (j + 1) / sqrt m := by suffices √(∑ i, ((hk.1 - (F x)) (S i)) ^ 2 / ↑m) ≤ ej c (j + 1) from by rw [<- Finset.sum_div] at this simp at this have u : √(∑ i, (hk.1 - F x) (S i) ^ 2) / ↑m = (√(∑ i, (hk.1 - F x) (S i) ^ 2) / √↑m) / √↑m := by field_simp congr apply Real.sq_sqrt exact Nat.cast_nonneg m rw [u] apply div_le_div_of_nonneg_right this simp have gh : hk.1 = chainApprox c_pos h' x ((j : ℕ) + 1) := by rw [<- fhx] rw [gh] have : √(∑ i, (chainApprox c_pos h' x ((j : ℕ) + 1) - F x) (S i) ^ 2 / ↑m) = empiricalDist S (F x) (chainApprox c_pos h' x ((j : ℕ) + 1)) := by rw [empiricalDist_comm] dsimp [empiricalDist, empiricalNorm] apply congrArg simp [div_eq_mul_inv, mul_comm] exact symm (Finset.mul_sum univ (fun i ↦ (chainApprox c_pos h' x (↑j + 1) (S i) - F x (S i)) ^ 2) (↑m)⁻¹) rw [this] dsimp only [ej] exact empiricalDist_to_chainApprox_le_ej c_pos h' x ((j : ℕ) + 1) cs have r1 : √(∑ i, ((hk.2 - (F x)) (S i)) ^ 2) / ↑m ≤ ej c j / sqrt m := by suffices √(∑ i, ((hk.2 - (F x)) (S i)) ^ 2 / ↑m) ≤ ej c j from by rw [<- Finset.sum_div] at this simp at this have u : √(∑ i, (hk.2 - F x) (S i) ^ 2) / ↑m = (√(∑ i, (hk.2 - F x) (S i) ^ 2) / √↑m) / √↑m := by field_simp congr apply Real.sq_sqrt exact Nat.cast_nonneg m rw [u] apply div_le_div_of_nonneg_right this simp have gh : hk.2 = chainApprox c_pos h' x j := by rw [<- fhx] rw [gh] have : √(∑ i, (chainApprox c_pos h' x j - F x) (S i) ^ 2 / ↑m) = empiricalDist S (F x) (chainApprox c_pos h' x j) := by rw [empiricalDist_comm] dsimp [empiricalDist, empiricalNorm] apply congrArg simp [div_eq_mul_inv, mul_comm] exact symm (Finset.mul_sum univ (fun i ↦ (chainApprox c_pos h' x (↑j) (S i) - F x (S i)) ^ 2) (↑m)⁻¹) rw [this] dsimp only [ej] exact empiricalDist_to_chainApprox_le_ej c_pos h' x j cs rw [rp] apply add_le_add r0 r1 · exact Real.sqrt_nonneg (2 * log (↑(coveringNumber' h' (ej c ((j : ℕ) + 1))) * ↑(coveringNumber' h' (ej c (j : ℕ))))) _ = ∑ j : Fin n, ((6 * (ej c (j + 1) - ej c (j + 2))) * (√(2 * log ((coveringNumber' h' (ej c (j + 1))) * (coveringNumber' h' (ej c j))))) / (sqrt m)) := by apply congrArg ext j field_simp _ ≤ ∑ j : Fin n, ((6 * (ej c (j + 1) - ej c (j + 2))) * (√(2 * log ((coveringNumber' h' (ej c (j + 1))) * (coveringNumber' h' (ej c (j + 1)))))) / (sqrt m)) := by refine Finset.sum_le_sum ?_ intro s si refine div_le_div_of_nonneg_right ?_ ?_ · refine mul_le_mul_of_nonneg_left ?_ ?_ · have NonemptyFS : Nonempty (EmpiricalFunctionSpace F S) := by rename_i h obtain ⟨i⟩ := h use i apply Real.sqrt_le_sqrt refine (mul_le_mul_iff_of_pos_left (by simp)).mpr ?_ apply Real.log_le_log refine Left.mul_pos ?_ ?_ repeat (norm_cast; apply coveringNumber'_nonzero; simp; apply ej_pos c_pos) refine (mul_le_mul_iff_of_pos_left (by norm_cast -- … truncated; follow the source link for the rest …
Causalean.Stat.Concentration.partB_bound · Causalean/Stat/Concentration/Covering/DudleyEntropy/PartB.lean:28 · uses EmpiricalFunctionSpace , chainApprox , coveringNumber' , ej , empiricalNorm , instPseudoMetricSpaceEmpiricalFunctionSpace , signs_card_inv
Part­BCore 3 core · 3 supporting This module contains the finite-class construction underlying the Part B chaining estimate. ★ partB_sum_bound_via_massart

This module contains the finite-class construction underlying the Part B chaining estimate. It uses the canonical Massart bound and exposes only the adjacent-pair finite set and the intermediate estimate needed by PartB.

def incrementPairSet reviewed
Causalean.Stat.Concentration

For a function class on a finite sample, a radius, positivity of that radius, total boundedness, a number of levels, and a level, this is the set of adjacent chaining-approximation pairs.

Definition (Lean source)
parameters
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
n :
ℕ
j :
Fin n
def
incrementPairSet c_pos h n j :
Set ((Z → ℝ) × (Z → ℝ))
given by
{(chainApprox c_pos h fh (j + 1), chainApprox c_pos h fh j) | fh : ι}
Causalean.Stat.Concentration.incrementPairSet · Causalean/Stat/Concentration/Covering/DudleyEntropy/PartBCore.lean:34 · uses EmpiricalFunctionSpace , instPseudoMetricSpaceEmpiricalFunctionSpace
def incrementPairFinset reviewed
Causalean.Stat.Concentration

For a function class on a finite sample, a radius, positivity of that radius, total boundedness, a number of levels, and a level, this is the finite set of distinct adjacent chaining-approximation pairs.

Definition (Lean source)
parameters
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h' :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
n :
ℕ
j :
Fin n
def
incrementPairFinset c_pos h' n j :
Finset ((Z → ℝ) × (Z → ℝ))
given by
Set.Finite.toFinset (finite_incrementPairSet c_pos h' n j)
Causalean.Stat.Concentration.incrementPairFinset · Causalean/Stat/Concentration/Covering/DudleyEntropy/PartBCore.lean:190 · uses EmpiricalFunctionSpace , instPseudoMetricSpaceEmpiricalFunctionSpace
lemma partB_sum_bound_via_massart reviewed
Causalean.Stat.Concentration

For a function class on a finite sample, a radius, positivity of that radius, total boundedness, a number of levels, positive sample size, a uniform empirical-radius bound, and at least one chaining level, the signed increment sum is bounded by the Massart finite-class expression over adjacent approximation pairs.

Formal statement
hypotheses
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h' :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
n :
ℕ
m_pos :
0 < m
cs :
∀ f : ι, empiricalNorm S (F f) ≤ c
n_pos :
0 < n
conclusion
∑ j : Fin n, ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((chainApprox c_pos h' fh (j + 1) - chainApprox c_pos h' fh j) (S i))))
≤ ∑ j : Fin n, (sup' (incrementPairFinset c_pos h' n j) (incrementPairFinset_nonempty c_pos h' n j) fun hk ↦ √(∑ i : Fin m, ((hk.1 - hk.2) (S i)) ^ 2)) * (√(2 * log (coveringNumber' h' (ej c (j + 1)) * coveringNumber' h' (ej c j)))) / ↑m
Proof (Lean source)
lemma partB_sum_bound_via_massart (c_pos : 0 < c) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : 0 < m) (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) (n_pos : 0 < n) : ∑ j : Fin n, ((m : ℝ)⁻¹ * signs_card_inv m * ∑ σ : Signs m, ⨆ fh : ι, (∑ i : Fin m, (σ i : ℝ) * ((chainApprox c_pos h' fh (j + 1) - chainApprox c_pos h' fh j) (S i)))) ≤ ∑ j : Fin n, (sup' (incrementPairFinset c_pos h' n j) (incrementPairFinset_nonempty c_pos h' n j) fun hk ↦ √(∑ i : Fin m, ((hk.1 - hk.2) (S i)) ^ 2)) * (√(2 * log (coveringNumber' h' (ej c (j + 1)) * coveringNumber' h' (ej c j)))) / ↑m := by -- It suffices to prove the bound term-by-term in the finite sum over j. apply Finset.sum_le_sum intro j hj -- Replace the supremum over f with a finite supremum over the paired class. calc _ ≤ ((incrementFinset c_pos h' n j).sup' (incrementFinset_nonempty c_pos h' n j) fun j ↦ √(∑ i, (|j (S i)|) ^ 2)) * (√(2 * log ((Set.Finite.toFinset (finite_incrementSet c_pos h' n j)).card))) / m := massart_bound_for_increment_term c_pos h' n j m_pos cs _ ≤ ((sup' (incrementPairFinset c_pos h' n j) (incrementPairFinset_nonempty c_pos h' n j) fun hk ↦ √(∑ i : Fin m, ((hk.1 - hk.2) (S i) ) ^ 2)) * (√(2 * log ((Set.Finite.toFinset (finite_incrementSet c_pos h' n j)).card)))) / m := by apply div_le_div_of_nonneg_right _ _ apply mul_le_mul_of_nonneg_right _ _ apply Finset.sup'_le _ _ intro hk hk0 simp only [Set.Finite.mem_toFinset, incrementFinset] at hk0 obtain ⟨fh, hfh⟩ := hk0 rw [<- hfh] have : √(∑ i, |(chainApprox c_pos h' fh ((j : ℕ) + 1) - chainApprox c_pos h' fh (j : ℕ)) (S i)| ^ 2) = √(∑ i : Fin m, ((chainApprox c_pos h' fh ((j : ℕ) + 1) - chainApprox c_pos h' fh (j : ℕ)) (S i)) ^ 2) := by congr ext i exact sq_abs _ rw [this] have : ⟨chainApprox c_pos h' fh ((j : ℕ) + 1), chainApprox c_pos h' fh (j : ℕ)⟩ ∈ incrementPairFinset c_pos h' n j := by simp only [Set.Finite.mem_toFinset, incrementPairFinset, incrementPairSet] use fh exact Finset.le_sup' (fun hk : (Z → ℝ) × (Z → ℝ) ↦ sqrt (∑ i : Fin m, ((hk.1 - hk.2) (S i) ) ^ 2)) this simp simp _ ≤ _ := by refine div_le_div_of_nonneg_right ?_ ?_ · apply mul_le_mul_of_nonneg_left · apply Real.sqrt_le_sqrt refine mul_le_mul_of_nonneg_left ?_ (by simp) apply Real.log_le_log · simp exact (Set.Finite.toFinset_nonempty (finite_incrementSet c_pos h' n j)).mp (incrementFinset_nonempty c_pos h' n j) · norm_cast apply (incrementFinset_card_le_incrementPairFinset_card c_pos h' n j).trans refine (incrementPairFinset_card_le_cover_product_card c_pos h' n j n_pos).trans_eq ?_ simp only [coveringFinset_card] · obtain ⟨fh⟩ := (by assumption : Nonempty ι) have hem : ⟨chainApprox c_pos h' fh (j + 1), chainApprox c_pos h' fh j⟩ ∈ incrementPairFinset c_pos h' n j := by simp only [Set.Finite.mem_toFinset, incrementPairFinset, incrementPairSet] use fh apply le_trans _ (Finset.le_sup' _ hem) apply Real.sqrt_nonneg · simp
Causalean.Stat.Concentration.partB_sum_bound_via_massart · Causalean/Stat/Concentration/Covering/DudleyEntropy/PartBCore.lean:568 · uses EmpiricalFunctionSpace , chainApprox , coveringNumber' , ej , empiricalNorm , incrementPairFinset , incrementPairFinset_nonempty , instPseudoMetricSpaceEmpiricalFunctionSpace , signs_card_inv
3 supporting declarations (lemmas, instances)
Riemann­Integral 1 core · 1 supporting This file converts the dyadic sum of square-root log covering numbers into a Riemann integral and chooses the dyadic truncation scale associated with a positive lower cutoff. ★ entropy_sum_to_integral_bound

Entropy sums and their integral bound

This file converts the dyadic sum of square-root log covering numbers into a Riemann integral and chooses the dyadic truncation scale associated with a positive lower cutoff. These are the analytic estimates used by the final Dudley entropy theorem.

lemma entropy_sum_to_integral_bound reviewed
Causalean.Stat.Concentration

For a function class evaluated on a finite sample, a positive empirical radius, positivity of that radius, total boundedness of the empirical class, a terminal chaining level, positive sample size, and a uniform empirical-radius bound, the empirical Rademacher complexity is bounded by a terminal dyadic remainder plus the entropy integral from that scale to half the radius.

Formal statement
hypotheses
Z :
Type v
shared
m :
ℕ
shared
ι :
Type u
ι → Z → ℝ
shared
S :
Fin m → Z
shared
c :
ℝ
shared
c_pos :
0 < c
h' :
TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))
n :
ℕ
m_pos :
0 < m
cs :
∀ f : ι, empiricalNorm S (F f) ≤ c
conclusion
empiricalRademacherComplexity_without_abs m F S
≤ 2 * (ej c (n+1))
+ 12 / (sqrt m)*(∫ (x : ℝ) in (ej c (n+1))..(c/2),√(log (coveringNumber' h' x)))
Proof (Lean source)
lemma entropy_sum_to_integral_bound (c_pos : 0 < c) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : 0 < m) (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) : empiricalRademacherComplexity_without_abs m F S ≤ 2 * (ej c (n+1)) + 12 / (sqrt m)*(∫ (x : ℝ) in (ej c (n+1))..(c/2),√(log (coveringNumber' h' x))) := by calc _ ≤ (ej c n) + 12 / (sqrt m)*(∑ j : Fin n, ((ej c (j+1) - ej c (j+2))*√(log (coveringNumber' h' (ej c (j+1)))))) := combine_partA_partB c_pos h' n m_pos cs _ = 2 * (ej c (n+1)) + 12 / (sqrt m)*(∑ j : Fin n, ((ej c (j+1) - ej c (j+2))*√(log (coveringNumber' h' (ej c (j+1)))))) := by refine add_right_cancel_iff.mpr ?_ dsimp [ej] grind _ ≤ _ := by suffices (∑ j : Fin n, ((ej c (j+1) - ej c (j+2))*√(log (coveringNumber' h' (ej c (j+1)))))) ≤ (∫ (x : ℝ) in (ej c (n + 1))..(c/2),√(log (coveringNumber' h' x))) from by refine (add_le_add_iff_left (2 * ej c (n + 1))).mpr ?_ apply mul_le_mul_of_nonneg_left exact this refine div_nonneg ?_ ?_ simp simp let f := fun (x : ℕ) ↦ ej c (x + 1) have : c / 2 = ej c 1 := by dsimp [ej] simp rw [this] let g := fun x ↦ √(log ↑(coveringNumber' h' x)) suffices ∑ j : Fin n, (f j - f (j + 1)) * g (f j) ≤ ∫ (x : ℝ) in f n..f 0, g x from by dsimp [f, g] at this have p (j : Fin n) : (j : ℕ) + 1 + 1 = (j : ℕ) + 2 := by ring apply le_of_eq_of_le rfl exact this have s : 0 < f n := by dsimp [f] dsimp [ej] simp exact c_pos apply AntitoneOn.leftRiemann_sum_le_integral · dsimp [f] refine Antitone.covariant_of_const' ?_ 1 apply ej_antitone apply le_of_lt c_pos · dsimp [g] have f0 : Monotone (fun x ↦ √x) := by apply Real.sqrt_le_sqrt apply Monotone.comp_antitoneOn f0 refine antitoneOn_iff_forall_lt.mpr ?_ intro a ha b hb hab apply Real.log_le_log · apply Nat.cast_pos.mpr apply coveringNumber'_nonzero · exact e_nonempty simp at hb linarith norm_cast apply coveringNumber'_antitone simp simp at ha linarith simp simp at hb linarith apply le_of_lt hab
Causalean.Stat.Concentration.entropy_sum_to_integral_bound · Causalean/Stat/Concentration/Covering/DudleyEntropy/RiemannIntegral.lean:262 · uses EmpiricalFunctionSpace , coveringNumber' , ej , empiricalNorm , instPseudoMetricSpaceEmpiricalFunctionSpace
1 supporting declaration (lemmas, instances)
  • choose_dyadic_scale_for_epsilon lemma — If the target scale is positive and smaller than half the initial radius, then some dyadic chaining radius lies strictly above the target scale and at most twice it.
    hypotheses
    c :
    ℝ
    shared
    ε :
    ℝ
    ε_pos :
    0 < ε
    c_ε :
    ε < c / 2
    conclusion
    ∃ n,
    conclusion 1
    ε < (ej c (n+1))
    conclusion 2
    (ej c (n+1)) ≤ 2 * ε
    Proof (Lean source)
    lemma choose_dyadic_scale_for_epsilon (ε : ℝ) (ε_pos : 0 < ε) (c_ε : ε < c / 2) : ∃ n, (ε < (ej c (n+1))) ∧ ((ej c (n+1)) ≤ 2 * ε) := by dsimp [ej] suffices ∃ n : ℕ, n < Real.logb 2 (c / ε) ∧ Real.logb 2 (c / ε) ≤ n + 1 from by obtain ⟨m0, ⟨hm1, hm2⟩⟩ := this rw [Real.logb_le_iff_le_rpow] at hm2 rw [Real.lt_logb_iff_rpow_lt] at hm1 have r : 0 < m0 := by have r0 : 2 < c / ε := by have r00 : 2 * ε < c := by refine (lt_div_iff₀' ?_).mp c_ε norm_num exact (lt_div_iff₀ ε_pos).mpr r00 have r1 : (2 : ℝ) < (2 : ℝ) ^ (↑m0 + 1) := by norm_cast at hm2 apply lt_of_lt_of_le r0 norm_cast rcases Nat.eq_zero_or_pos m0 with h0 | h0 · rw [h0] at r1 norm_num at r1 · exact h0 have p0 : ε < c / 2 ^ (↑m0) := by have htmp := mul_lt_mul_of_pos_right hm1 ε_pos have htmp_mul : ε * 2 ^ (↑m0) < c := by field_simp at htmp simp at htmp rw [mul_comm] exact htmp have hpowpos : 0 < (2 : ℝ) ^ (↑m0) := pow_pos (by norm_num) _ have := mul_lt_mul_of_pos_right htmp_mul (inv_pos.mpr hpowpos) simpa [mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv] using this have p1 : c / 2 ^ (↑m0) ≤ 2 * ε := by have htmp : c ≤ ε * 2 ^ (↑m0 + 1) := by have := mul_le_mul_of_nonneg_left hm2 (le_of_lt ε_pos) field_simp at this norm_cast at this norm_cast have hpowpos : 0 < (2 : ℝ) ^ (↑m0) := pow_pos (by norm_num) _ have hpow_ne : (2 : ℝ) ^ (↑m0) ≠ 0 := by exact ne_of_gt hpowpos calc c / 2 ^ (↑m0) = c * ((2 : ℝ) ^ (↑m0))⁻¹ := by simp [div_eq_mul_inv] _ ≤ (ε * 2 ^ (↑m0 + 1)) * ((2 : ℝ) ^ (↑m0))⁻¹ := by exact mul_le_mul_of_nonneg_right htmp (inv_nonneg.mpr (le_of_lt hpowpos)) _ = ε * 2 := by simp [pow_succ, mul_comm, mul_assoc, hpow_ne] _ = 2 * ε := by ring use (m0 - 1) have : m0 - 1 + 1 = m0 := by grind rw [this] exact ⟨p0, p1⟩ · norm_num · field_simp linarith · norm_num · field_simp linarith use Int.toNat (Int.ceil (Real.logb 2 (c / ε))) - 1 have h3 : 0 < Real.logb 2 (c / ε) := by refine Real.logb_pos (by linarith) ?_ refine (one_lt_div₀ ε_pos).mpr ?_ apply lt_trans c_ε linarith have h2 : ((⌈Real.logb 2 (c / ε)⌉ : ℤ) : ℝ) = ((⌈Real.logb 2 (c / ε)⌉.toNat : ℕ) : ℝ) := by norm_cast refine Int.eq_natCast_toNat.mpr ?_ exact Int.ceil_nonneg (le_of_lt h3) have : (1 : ℤ) ≤ ⌈Real.logb 2 (c / ε)⌉ := by simpa using Int.one_le_ceil_iff.mpr h3 have hceil_nonneg : 0 ≤ ⌈Real.logb 2 (c / ε)⌉ := Int.ceil_nonneg (le_of_lt h3) have hcast : Int.ofNat (⌈Real.logb 2 (c / ε)⌉.toNat) = ⌈Real.logb 2 (c / ε)⌉ := Int.toNat_of_nonneg hceil_nonneg have h_nat : 1 ≤ ⌈Real.logb 2 (c / ε)⌉.toNat := by have : (Int.ofNat 1) ≤ Int.ofNat (⌈Real.logb 2 (c / ε)⌉.toNat) := by simpa [hcast] using this exact (Int.ofNat_le).1 this constructor · rw [Nat.cast_sub] rw [<- h2] simp rw [<- Int.le_ceil_iff] simpa using h_nat · norm_cast have : ⌈Real.logb 2 (c / ε)⌉.toNat - 1 + 1 = ⌈Real.logb 2 (c / ε)⌉.toNat := by exact Nat.sub_add_cancel h_nat rw [this] rw [<- h2] exact Int.le_ceil (Real.logb 2 (c / ε))
    Causalean.Stat.Concentration.choose_dyadic_scale_for_epsilon · Causalean/Stat/Concentration/Covering/DudleyEntropy/RiemannIntegral.lean:327