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
suffices :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      Convex ℝ U →
        ∀ᶠ (n : ℕ) in atTop,
          ∀ (x : (↑I : Type)),
            gauge U
                (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
                  ((f : (a : (↑I : Type)) → E) x : E)) <
              1
⊢ Tendsto (fun (n : ℕ) ↦ bernsteinApproximation n f) atTop (𝓝 f)

Tactic:
suffices ∀ U ∈ 𝓝 (0 : E), Convex ℝ U →
      ∀ᶠ n in atTop, ∀ x : I, gauge U (bernsteinApproximation n f x - f x) < 1 by
    rw [(LocallyConvexSpace.convex_basis_zero ℝ E).uniformity_of_nhds_zero_swapped
      |>.compactConvergenceUniformity_of_compact |> nhds_basis_uniformity |>.tendsto_right_iff]
    rintro U ⟨hU₀, hcU⟩
    filter_upwards [this U hU₀ hcU] with n hn x
    exact gauge_lt_one_subset_self hcU (mem_of_mem_nhds hU₀) (absorbent_nhds_zero hU₀) (hn x)
-- 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 funProp : Convex ℝ U
funProp₁ : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type) × (↑I : Type)) ↦
    match (motive := (↑I : Type) × (↑I : Type) → ℝ) x with
    | (x, y) =>
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E))

Tactic:
fun_prop
-- 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
⊢ Continuous (Y := ℝ) fun (x : (↑I : Type) × (↑I : Type)) ↦
    match (motive := (↑I : Type) × (↑I : Type) → ℝ) x with
    | (x, y) =>
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E))

Tactic:
have : Continuous fun (x, y) ↦ gauge U (f x - f y) := by fun_prop
-- 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_2 : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
this :
  Continuous (Y := ℝ) fun (x : (↑I : Type) × (↑I : Type)) ↦
    match (motive := (↑I : Type) × (↑I : Type) → ℝ) x with
    | (x, y) =>
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E))
⊢ ∃ (C : ℝ),
    ∀ (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

Tactic:
simpa only [BddAbove, Set.Nonempty, mem_upperBounds, Set.forall_mem_range, Prod.forall]
      using isCompact_range this |>.bddAbove

Premises used: Set.forall_mem_range, IsCompact.bddAbove, BddAbove, isCompact_range, Set.Nonempty, Prod.forall, mem_upperBounds
-- 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
obtain :
  ∀ (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),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : (↑I : Type)),
        gauge U
            (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
              ((f : (a : (↑I : Type)) → E) x : E)) <
          1
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1

Tactic:
obtain ⟨C, hC⟩ : ∃ C, ∀ x y, gauge U (f x - f y) ≤ C := by
    have : Continuous fun (x, y) ↦ gauge U (f x - f y) := by fun_prop
    simpa only [BddAbove, Set.Nonempty, mem_upperBounds, Set.forall_mem_range, Prod.forall]
      using isCompact_range this |>.bddAbove
-- 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
⊢ 0 ≤ C

Tactic:
have hC₀ : 0 ≤ C := le_trans (gauge_nonneg _) (hC 0 0)
-- 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
⊢ UniformContinuous (α := (↑I : Type)) (β := E) (⇑f : (a : (↑I : Type)) → E)

Tactic:
have := CompactSpace.uniformContinuous_of_continuous (map_continuous f)
-- 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_2 : 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
this : UniformContinuous (α := (↑I : Type)) (β := E) (⇑f : (a : (↑I : Type)) → E)
⊢ ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (x y : (↑I : Type)),
            Membership.mem (γ := SetRel (↑I : Type) (↑I : Type)) {p : (↑I : Type) × (↑I : Type) | dist p.1 p.2 < j}
                (x, y) →
              Membership.mem (α := E × E) (γ := Set (E × E)) {x : E × E | x.1 - x.2 ∈ id i}
                (((f : (a : (↑I : Type)) → E) x, (f : (a : (↑I : Type)) → E) y) : E × E)

Tactic:
rw [Metric.uniformity_basis_dist.uniformContinuous_iff
      (basis_sets _).uniformity_of_nhds_zero_swapped] at this

Premises used: Metric.uniformity_basis_dist, Filter.basis_sets, Filter.HasBasis.uniformContinuous_iff, Filter.HasBasis.uniformity_of_nhds_zero_swapped
-- 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_2 : 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
this :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (x y : (↑I : Type)),
            Membership.mem (γ := SetRel (↑I : Type) (↑I : Type)) {p : (↑I : Type) × (↑I : Type) | dist p.1 p.2 < j}
                (x, y) →
              Membership.mem (α := E × E) (γ := Set (E × E)) {x : E × E | x.1 - x.2 ∈ id i}
                (((f : (a : (↑I : Type)) → E) x, (f : (a : (↑I : Type)) → E) y) : E × E)
⊢ 0 < 1 / 2

Tactic:
positivity
-- 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_2 : 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
this :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (x y : (↑I : Type)),
            Membership.mem (γ := SetRel (↑I : Type) (↑I : Type)) {p : (↑I : Type) × (↑I : Type) | dist p.1 p.2 < j}
                (x, y) →
              Membership.mem (α := E × E) (γ := Set (E × E)) {x : E × E | x.1 - x.2 ∈ id i}
                (((f : (a : (↑I : Type)) → E) x, (f : (a : (↑I : Type)) → E) y) : E × E)
⊢ ∃ δ > 0,
    ∀ (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

Tactic:
exact this {z | gauge U z < 1 / 2} <| tendsto_gauge_nhds_zero hU₀
      |>.eventually_lt_const <| by positivity

Premises used: gauge, setOf, HDiv.hDiv, Filter.Tendsto.eventually_lt_const, tendsto_gauge_nhds_zero, LT.lt, OfNat.ofNat
-- 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
obtain :
  ∀ (δ : ℝ) (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),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x : (↑I : Type)),
        gauge U
            (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
              ((f : (a : (↑I : Type)) → E) x : E)) <
          1
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1

Tactic:
obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0, ∀ x y : I, dist x y < δ → gauge U (f x - f y) < 1 / 2 := by
    have := CompactSpace.uniformContinuous_of_continuous (map_continuous f)
    rw [Metric.uniformity_basis_dist.uniformContinuous_iff
      (basis_sets _).uniformity_of_nhds_zero_swapped] at this
    exact this {z | gauge U z < 1 / 2} <| tendsto_gauge_nhds_zero hU₀
      |>.eventually_lt_const <| by positivity
-- 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
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)

Tactic:
have nhds_zero := tendsto_const_div_atTop_nhds_zero_nat (C / δ ^ 2)
-- 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)
h :
  ∀ (n : ℕ) (nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2) (hn₀ : n ≠ 0) (x : (↑I : Type)),
    gauge U
        (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
          ((f : (a : (↑I : Type)) → E) x : E)) <
      1
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x : (↑I : Type)),
      gauge U
          (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
            ((f : (a : (↑I : Type)) → E) x : E)) <
        1

Tactic:
filter_upwards [nhds_zero.eventually_lt_const (half_pos one_pos), eventually_ne_atTop 0]
    with n nh hn₀ x

Premises used: half_pos, Filter.eventually_ne_atTop, Filter.Tendsto.eventually_lt_const, OfNat.ofNat, one_pos
-- 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 < δ}
⊢ gauge U
      (HSub.hSub (α := E) (β := E) ((bernsteinApproximation n f : (a : (↑I : Type)) → E) x : E)
        ((f : (a : (↑I : Type)) → E) x : E)) =
    gauge U
      (∑ k : Fin (n + 1),
        HSMul.hSMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)))

Tactic:
simp [bernsteinApproximation.apply, smul_sub, ← Finset.sum_smul]

Premises used: Finset.sum_smul, smul_sub, bernsteinApproximation.apply
-- 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 < δ}
⊢ gauge U
      (∑ k : Fin (n + 1),
        HSMul.hSMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) ≤
    ∑ k : Fin (n + 1),
      gauge U
        (HSMul.hSMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E)))

Tactic:
gauge_sum_le hUc (absorbent_nhds_zero hU₀) _ _

Premises used: absorbent_nhds_zero, gauge_sum_le
-- 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 < δ}
⊢ Eq (α := ℝ)
    (∑ k : Fin (n + 1),
      gauge U
        (HSMul.hSMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k : Fin (n + 1),
      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))))

Tactic:
simp only [gauge_smul_of_nonneg, bernstein_nonneg, smul_eq_mul]

Premises used: gauge_smul_of_nonneg, bernstein_nonneg, smul_eq_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),
      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))) =
    HAdd.hAdd (α := ℝ)
      (∑ 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 (α := ℝ) ((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))))

Tactic:
(S.sum_add_sum_compl _).symm

Premises used: Eq.symm, Finset.sum_add_sum_compl
-- 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 < δ}
⊢ HAdd.hAdd (α := ℝ)
      (∑ 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 (α := ℝ) ((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 + 1 / 2

Tactic:
add_lt_add_of_le_of_lt ?_ ?_

Premises used: add_lt_add_of_le_of_lt
-- 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 / 2 + 1 / 2 = 1

Tactic:
add_halves 1

Premises used: add_halves, OfNat.ofNat