awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
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 : ℝ)
⊢ 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 : ℝ)

Tactic:
gcongr with k hk
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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ᶜ
rw : HMul.hMul (α := ℝ) (β := ℝ) (1 : ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
| (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x

Tactic:
rw [← one_mul (bernstein _ _ _)]

Premises used: bernstein, DFunLike.coe, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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ᶜ
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 : ℝ)
⊢ (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 _ _ _)]

Premises used: bernstein, DFunLike.coe, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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ᶜ
hbc : 1 ≤ HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2
⊢ 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:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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ᶜ
⊢ 1 ≤ HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2

Tactic:
simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using hk

Premises used: sq_le_sq, dist_comm, Real.dist_eq, abs_of_pos, one_le_div₀, Subtype.val
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
hbc : Sᶜ ⊆ Finset.univ
⊢ 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 : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
⊢ Sᶜ ⊆ Finset.univ

Tactic:
Sᶜ.subset_univ

Premises used: Compl.compl, Finset.subset_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
⊢ Sᶜ ⊆ Finset.univ

Tactic:
exact Sᶜ.subset_univ

Premises used: Compl.compl, Finset.subset_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 / HPow.hPow (β := ℕ) δ 2)
          ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    (C *
        ∑ k : Fin (n + 1),
          HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2)
            ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)) /
      HPow.hPow (β := ℕ) δ 2

Tactic:
simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]

Premises used: mul_div_assoc, mul_div_right_comm, Finset.sum_div
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
rw :
  C * ((↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)) / HPow.hPow (β := ℕ) δ 2 =
    C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)
⊢ (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 : ℝ)

Tactic:
rw [variance hn₀]

Premises used: bernstein.variance
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 * ((↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)) / HPow.hPow (β := ℕ) δ 2 =
    C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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
hab₂ : 1 - (↑x : ℝ) ≤ 1
⊢ C / HPow.hPow (β := ℕ) δ 2 * (↑x : ℝ) * (1 - (↑x : ℝ)) / (↑n : ℝ) ≤ C / HPow.hPow (β := ℕ) δ 2 * 1 * 1 / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
⊢ 0 ≤ 1 - (↑x : ℝ)

Tactic:
unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
⊢ (↑x : ℝ) ≤ 1

Tactic:
unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 < δ}
⊢ 1 - (↑x : ℝ) ≤ 1

Tactic:
unit_interval
-- Module: Mathlib.Analysis.SpecialFunctions.Bernstein
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 * 1 * 1 / (↑n : ℝ) < 1 / 2

Tactic:
simpa only [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ binEntropy 0 = 0

Tactic:
simp [binEntropy]

Premises used: Real.binEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ binEntropy 1 = 0

Tactic:
simp [binEntropy]

Premises used: Real.binEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
norm_num : 1 / 2 * log 2 + 1 / 2 * log 2 = log 2
⊢ binEntropy 2⁻¹ = log 2

Tactic:
norm_num [binEntropy]

Premises used: Real.binEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
simp : 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2
⊢ 1 / 2 * log 2 + 1 / 2 * log 2 = log 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
⊢ binEntropy p = p.negMulLog + (1 - p).negMulLog

Tactic:
simp [binEntropy, negMulLog, ← neg_mul]

Premises used: Real.binEntropy, Real.negMulLog, neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ binEntropy = fun (p : ℝ) ↦ p.negMulLog + (1 - p).negMulLog

Tactic:
funext binEntropy_eq_negMulLog_add_negMulLog_one_sub

Premises used: funext, Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
⊢ binEntropy (1 - p) = binEntropy p

Tactic:
simp [binEntropy, add_comm]

Premises used: Real.binEntropy, add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
rw : binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)
⊢ binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

Tactic:
rw [← binEntropy_one_sub]

Premises used: Real.binEntropy_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < 1 - p

Tactic:
have : 0 < 1 - p := sub_pos.2 hp₁
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < 1 - p
⊢ 0 < log p⁻¹

Tactic:
have : 0 < log p⁻¹ := log_pos <| (one_lt_inv₀ hp₀).2 hp₁
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this_1 : 0 < 1 - p
this : 0 < log p⁻¹
⊢ 0 < log (1 - p)⁻¹

Tactic:
have : 0 < log (1 - p)⁻¹ := log_pos <| (one_lt_inv₀ ‹_›).2 (sub_lt_self _ hp₀)
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this_1 : 0 < 1 - p
this_2 : 0 < log p⁻¹
this : 0 < log (1 - p)⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1), 0 ≤ binEntropy 0
inr : ∀ (hp₀ : 0 < p), 0 ≤ binEntropy p
⊢ 0 ≤ binEntropy p

Tactic:
obtain rfl | hp₀ := hp₀.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
hp₀ : LE.le (α := ℝ) 0 0
hp₁ : LE.le (α := ℝ) 0 1
⊢ 0 ≤ binEntropy 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1), 0 ≤ binEntropy 1
inr₁ : ∀ (hp₁ : p < 1), 0 ≤ binEntropy p
⊢ 0 ≤ binEntropy p

Tactic:
obtain rfl | hp₁ := hp₁.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl