awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ LE.le (α := ℝ)
    (∑ x_1 ∈ Sᶜ,
      HMul.hMul (β := ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x_1/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)))
        ((bernstein n (↑x_1 : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
    (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
have h : ∀ i ∈ Sᶜ,
  gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) i/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)) ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ ∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
have rw : Eq (α := ℝ) (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
  (∑ i ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑i : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
Tactic: rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
    C *
      ∑ k ∈ Sᶜ,
        HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
          ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
have hbc : ∀ (k : Fin (n + 1)) (hk : k ∈ Sᶜ),
  (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
      ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
Tactic: gcongr with k hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k : Fin (n + 1)
hk : k ∈ Sᶜ
| (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
have rw : HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
Tactic: rw [← one_mul (bernstein _ _ _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k : Fin (n + 1)
hk : k ∈ Sᶜ
⊢ (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
      ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
have hbc : HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) ≤
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
    ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
Tactic: conv_lhs => rw [← one_mul (bernstein _ _ _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k : Fin (n + 1)
hk : k ∈ Sᶜ
⊢ HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
      ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
have hbc : 1 ≤ HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ C *
      ∑ k ∈ Sᶜ,
        HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
          ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) ≤
    C *
      ∑ k : Fin (n + 1),
        HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
          ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
have hbc : Sᶜ ⊆ Finset.univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ (C *
        ∑ k : Fin (n + 1),
          HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2)
            ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)) /
      HPow.hPow (β := ℕ) δ 2 =
    C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)
have rw : C * ((↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)) / HPow.hPow (β := ℕ) δ 2 =
  C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)
Tactic: rw [variance hn₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) ≤ C / HPow.hPow (β := ℕ) δ 2 * 1 * 1 / (↑n : ℝ)
have hab : 0 ≤ 1 - (↑x : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
hab : 0 ≤ 1 - (↑x : ℝ)
⊢ C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) ≤ C / HPow.hPow (β := ℕ) δ 2 * 1 * 1 / (↑n : ℝ)
have hab₁ : (↑x : ℝ) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
hab : 0 ≤ 1 - (↑x : ℝ)
hab₁ : (↑x : ℝ) ≤ 1
⊢ C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) ≤ C / HPow.hPow (β := ℕ) δ 2 * 1 * 1 / (↑n : ℝ)
have hab₂ : 1 - (↑x : ℝ) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
⊢ ∑ k ∈ Sᶜ,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) <
    1 / 2
have k : LE.le (α := ℝ)
  (∑ k ∈ Sᶜ,
    HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
      (gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
  (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
Tactic: calc
      ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * bernstein n k x := by
        simp only [mul_comm (bernstein n _ x)]
        gcongr
        apply hC
      _ = C * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
      _ ≤ C * ∑ k ∈ Sᶜ, ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr with k hk
        conv_lhs => rw [← one_mul (bernstein _ _ _)]
        gcongr
        simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using hk
      -- Again enlarging the sum from `Sᶜ` to all of `Fin (n+1)`
      _ ≤ C * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr; exact Sᶜ.subset_univ
      _ = C * (∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x) / δ ^ 2 := by
        simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]
      -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
      _ = C / δ ^ 2 * x * (1 - x) / n := by rw [variance hn₀]; ring
      _ ≤ C / δ ^ 2 * 1 * 1 / n := by gcongr <;> unit_interval
      _ < 1 / 2 := by simpa only [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k :
  LE.le (α := ℝ)
    (∑ k ∈ Sᶜ,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
⊢ ∑ k ∈ Sᶜ,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) <
    1 / 2
have k₁ : ∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
  C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
Tactic: calc
      ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * bernstein n k x := by
        simp only [mul_comm (bernstein n _ x)]
        gcongr
        apply hC
      _ = C * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
      _ ≤ C * ∑ k ∈ Sᶜ, ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr with k hk
        conv_lhs => rw [← one_mul (bernstein _ _ _)]
        gcongr
        simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using hk
      -- Again enlarging the sum from `Sᶜ` to all of `Fin (n+1)`
      _ ≤ C * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr; exact Sᶜ.subset_univ
      _ = C * (∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x) / δ ^ 2 := by
        simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]
      -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
      _ = C / δ ^ 2 * x * (1 - x) / n := by rw [variance hn₀]; ring
      _ ≤ C / δ ^ 2 * 1 * 1 / n := by gcongr <;> unit_interval
      _ < 1 / 2 := by simpa only [mul_one]