awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
mp : ‖f x‖ₑ ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ
⊢ ‖f x‖ ≤ (↑(‖c‖₊ / r) : ℝ) * ‖g x‖

Tactic:
suffices ‖f x‖ₑ ≤ (‖c‖₊ / r : ℝ≥0) * ‖g x‖ₑ by
      simp only [enorm_eq_nnnorm, ← coe_nnnorm] at this ⊢
      exact mod_cast this
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
⊢ ‖f x‖ₑ ≤ egauge 𝕜 (ball 0 1) (f x)

Tactic:
le_egauge_ball_one ..

Premises used: le_egauge_ball_one
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
⊢ egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)

Tactic:
hx
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x) ≤ ‖c‖ₑ * ‖g x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'

Premises used: egauge_ball_le_of_one_lt_norm, LT.lt.ne', Or.inl
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
⊢ ‖c‖ₑ * ‖g x‖ₑ / (↑r : ℝ≥0∞) = (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ

Tactic:
simp [hr₀.ne', ENNReal.mul_div_right_comm, enorm_eq_nnnorm]

Premises used: ENNReal.mul_div_right_comm, LT.lt.ne', enorm_eq_nnnorm
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, _root_.egauge 𝕜 (ball 0 i) (f x) ≤ _root_.egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, _root_.egauge 𝕜 (ball 0 1) (f x) ≤ _root_.egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : _root_.egauge 𝕜 (ball 0 1) (f x) ≤ _root_.egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
egauge : ‖c‖ₑ * ‖g x‖ₑ / (↑r : ℝ≥0∞) = (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ
⊢ ‖f x‖ₑ ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ

Tactic:
calc
      ‖f x‖ₑ ≤ egauge 𝕜 (ball 0 1) (f x) := le_egauge_ball_one ..
      _ ≤ egauge 𝕜 (ball 0 r) (g x) := hx
      _ ≤ ‖c‖ₑ * ‖g x‖ₑ / ↑r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ = (‖c‖₊ / r : ℝ≥0) * ‖g x‖ₑ := by
        simp [hr₀.ne', ENNReal.mul_div_right_comm, enorm_eq_nnnorm]

Premises used: egauge_ball_le_of_one_lt_norm, NNNorm.nnnorm, HDiv.hDiv, Metric.ball, le_egauge_ball_one, OfNat.ofNat, egauge, NNReal.toReal
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
mpr :
  (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
⊢ f =O[l] g → f =O[𝕜; l] g

Tactic:
rw [nhds_basis_ball.isBigOTVS_iff nhds_basis_ball, isBigO_iff']

Premises used: Filter.HasBasis.isBigOTVS_iff, Metric.nhds_basis_ball, Asymptotics.isBigO_iff'
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
r : ℝ
hr₀ : 0 < r
⊢ 0 ≤ C

Tactic:
hC₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
r : ℝ
hr₀ : 0 < r
mpr :
  ∀ (C : ℝ≥0) (hC₀ : (↑C : ℝ) > 0) (hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖),
    ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)

Tactic:
lift C to ℝ≥0 using hC₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
r : ℝ
hr₀ : 0 < r
C : ℝ≥0
hC₀ : (↑C : ℝ) > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ 0 < C

Tactic:
norm_cast at hC₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
r : ℝ
hr₀ : 0 < r
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
⊢ 0 ≤ r

Tactic:
hr₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
r : ℝ
hr₀ : 0 < r
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
mpr :
  ∀ (r : ℝ≥0) (hr₀ : 0 < (↑r : ℝ)),
    ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)

Tactic:
lift r to ℝ≥0 using hr₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ)
⊢ 0 < r

Tactic:
norm_cast at hr₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
⊢ 0 < (↑r : ℝ) / ((↑C : ℝ) * (↑‖c‖₊ : ℝ))

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
mpr :
  ∀ (x : α) (hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖),
    egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 ((↑r : ℝ) / ((↑C : ℝ) * (↑‖c‖₊ : ℝ)))) (g x)
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)

Tactic:
refine ⟨r / (C * ‖c‖₊), by positivity, hC.mono fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ ‖c‖ₑ * ‖f x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'

Premises used: egauge_ball_le_of_one_lt_norm, LT.lt.ne', Or.inl
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hab : ‖f x‖ₑ ≤ (↑C : ℝ≥0∞) * ‖g x‖ₑ
⊢ ‖c‖ₑ * ‖f x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : (↑‖f x‖₊ : ℝ) ≤ (↑C : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
mod_cast hx

Premises used: ENNReal.ofNNReal, NNReal.coe_le_coe._simp_1, cast, WithTop.some, ENNReal.coe_le_coe._simp_1, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : (↑‖f x‖₊ : ℝ) ≤ (↑C : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑C : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
exact mod_cast hx
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
simp_all :
  ∀ (hc₀ : ¬c = 0) (hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖) (hC₀ : ¬C = 0) (hr₀ : ¬r = 0)
    (hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖),
    (↑r : ℝ≥0∞)⁻¹ * (‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ)) = (↑C : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹ * ‖g x‖ₑ
⊢ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞) = ‖g x‖ₑ / (↑(r / (C * ‖c‖₊)) : ℝ≥0∞)

Tactic:
simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]

Premises used: ENNReal.mul_inv, pos_iff_ne_zero, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
C r : ℝ≥0
x : α
hc₀ : ¬c = 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : ¬C = 0
hr₀ : ¬r = 0
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ (↑r : ℝ≥0∞)⁻¹ * (‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ)) = (↑C : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹ * ‖g x‖ₑ

Tactic:
ac_rfl
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ ‖g x‖ₑ / (↑(r / (C * ‖c‖₊)) : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 (↑(r / (C * ‖c‖₊)) : ℝ)) (g x)

Tactic:
div_le_egauge_ball _ _ _

Premises used: div_le_egauge_ball
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
egauge : ‖c‖ₑ * ‖f x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞)
egauge₁ : ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞) = ‖g x‖ₑ / (↑(r / (C * ‖c‖₊)) : ℝ≥0∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ _root_.egauge 𝕜 (ball 0 ((↑r : ℝ) / ((↑C : ℝ) * (↑‖c‖₊ : ℝ)))) (g x)

Tactic:
calc
      egauge 𝕜 (ball 0 r) (f x) ≤ ‖c‖ₑ * ‖f x‖ₑ / r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ ≤ ‖c‖ₑ * (C * ‖g x‖ₑ) / r := by
        gcongr
        simp only [enorm_eq_nnnorm, ← coe_nnnorm] at hx ⊢
        exact mod_cast hx
      _ = ‖g x‖ₑ / (r / (C * ‖c‖₊) : ℝ≥0) := by
        simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]
        ac_rfl
      _ ≤ _ := div_le_egauge_ball _ _ _

Premises used: ENNReal.ofNNReal, egauge_ball_le_of_one_lt_norm, HMul.hMul, NNNorm.nnnorm, HDiv.hDiv, Metric.ball, ENorm.enorm, div_le_egauge_ball, OfNat.ofNat, egauge, NNReal.toReal
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
⊢ f =Θ[𝕜; l] g ↔ f =Θ[l] g

Tactic:
.and isBigOTVS_iff_isBigO isBigOTVS_iff_isBigO

Premises used: Asymptotics.isBigOTVS_iff_isBigO, Asymptotics.IsTheta, Iff.and, Asymptotics.IsThetaTVS
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
⊢ f =Θ[l] f

Tactic:
⟨isBigO_refl _ _, isBigO_refl _ _⟩

Premises used: Asymptotics.IsTheta, And.intro, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
f : α → E
l : Filter α
⊢ f =Θ[l] f

Tactic:
isTheta_refl _ _

Premises used: Asymptotics.isTheta_refl
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : f =Θ[l] g
⊢ g =Θ[l] f

Tactic:
h.symm

Premises used: Asymptotics.IsTheta, And.symm
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =Θ[l] g ↔ g =Θ[l] f

Tactic:
⟨fun h ↦ h.symm, fun h ↦ h.symm⟩

Premises used: Asymptotics.IsTheta.symm, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
h₁ : f =Θ[l] g
h₂ : g =Θ[l] k
⊢ f =Θ[l] k

Tactic:
⟨h₁.1.trans h₂.1, h₂.2.trans h₁.2⟩

Premises used: Asymptotics.IsTheta, Asymptotics.IsBigO.trans, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
h₁ : f =O[l] g
h₂ : g =Θ[l] k
⊢ f =O[l] k

Tactic:
h₁.trans h₂.1

Premises used: Asymptotics.IsBigO.trans, And.left
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
h₁ : f =Θ[l] g
h₂ : g =O[l] k
⊢ f =O[l] k

Tactic:
h₁.1.trans h₂

Premises used: Asymptotics.IsBigO.trans, And.left
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
G' : Type u_8
inst : Norm E
inst_1 : Norm F
inst_2 : SeminormedAddCommGroup G'
l : Filter α
f : α → E
g : α → F
k : α → G'
h₁ : f =o[l] g
h₂ : g =Θ[l] k
⊢ f =o[l] k

Tactic:
h₁.trans_isBigO h₂.1

Premises used: And.left, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
G : Type u_5
F' : Type u_7
inst : Norm E
inst_1 : Norm G
inst_2 : SeminormedAddCommGroup F'
l : Filter α
f : α → E
g : α → F'
k : α → G
h₁ : f =Θ[l] g
h₂ : g =o[l] k
⊢ f =o[l] k

Tactic:
h₁.1.trans_isLittleO h₂

Premises used: And.left, Asymptotics.IsBigO.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f : α → E
g₁ g₂ : α → F
h : f =Θ[l] g₁
hg : g₁ =ᶠ[l] g₂
⊢ f =Θ[l] g₂

Tactic:
⟨h.1.trans_eventuallyEq hg, hg.symm.trans_isBigO h.2⟩

Premises used: Asymptotics.IsTheta, Asymptotics.IsBigO.trans_eventuallyEq, And.right, And.left, And.intro, Filter.EventuallyEq.symm, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
l : Filter α
f₁ f₂ : α → E
g : α → F
hf : f₁ =ᶠ[l] f₂
h : f₂ =Θ[l] g
⊢ f₁ =Θ[l] g

Tactic:
⟨hf.trans_isBigO h.1, h.2.trans_eventuallyEq hf.symm⟩

Premises used: Asymptotics.IsTheta, Asymptotics.IsBigO.trans_eventuallyEq, And.right, And.left, And.intro, Filter.EventuallyEq.symm, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
inst : Norm E
l : Filter α
f g : α → E
h : f =ᶠ[l] g
⊢ f =Θ[l] g

Tactic:
h.trans_isTheta isTheta_rfl

Premises used: Filter.EventuallyEq.trans_isTheta, Asymptotics.isTheta_rfl
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
⊢ f =Θ[⊥] g

Tactic:
simp [IsTheta]

Premises used: Asymptotics.IsTheta
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
F : Type u_4
E' : Type u_6
inst : Norm F
inst_1 : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ IsTheta (E := ℝ) l (fun (x : α) ↦ ‖f' x‖) g ↔ f' =Θ[l] g

Tactic:
simp [IsTheta]

Premises used: Asymptotics.IsTheta
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (IsTheta (F := ℝ) l f fun (x : α) ↦ ‖g' x‖) ↔ f =Θ[l] g'

Tactic:
simp [IsTheta]

Premises used: Asymptotics.IsTheta
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
h : l.EventuallyEq (β := ℝ) (fun (x : α) ↦ ‖f x‖) fun (x : α) ↦ ‖g x‖
⊢ f =Θ[l] g

Tactic:
⟨.of_bound' h.le, .of_bound' h.symm.le⟩

Premises used: Asymptotics.IsTheta, Filter.EventuallyEq.le, And.intro, Asymptotics.IsBigO.of_bound', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E' : Type u_6
inst : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
g : α → ℝ
h : (fun (x : α) ↦ ‖f' x‖) =ᶠ[l] g
x : α
hx : (fun (x : α) ↦ ‖f' x‖) x = g x
⊢ Eq (α := ℝ) ((fun (x : α) ↦ ‖f' x‖) x) ((fun (x : α) ↦ ‖g x‖) x)

Tactic:
simp only [← hx, norm_norm]

Premises used: norm_norm
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
G : Type u_5
E' : Type u_6
F' : Type u_7
inst : Norm G
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
k : α → G
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ f' =o[l] k ↔ g' =o[l] k

Tactic:
⟨h.symm.trans_isLittleO, h.trans_isLittleO⟩

Premises used: Asymptotics.IsTheta.symm, Iff.intro, Asymptotics.IsTheta.trans_isLittleO
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
G' : Type u_8
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f : α → E
g' : α → F'
k' : α → G'
l : Filter α
h : g' =Θ[l] k'
⊢ f =o[l] g' ↔ f =o[l] k'

Tactic:
⟨fun H ↦ H.trans_isTheta h, fun H ↦ H.trans_isTheta h.symm⟩

Premises used: Asymptotics.IsTheta.symm, Asymptotics.IsLittleO.trans_isTheta, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
G : Type u_5
E' : Type u_6
F' : Type u_7
inst : Norm G
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
k : α → G
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ f' =O[l] k ↔ g' =O[l] k

Tactic:
⟨h.symm.trans_isBigO, h.trans_isBigO⟩

Premises used: Asymptotics.IsTheta.symm, Asymptotics.IsTheta.trans_isBigO, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
E : Type u_3
F' : Type u_7
G' : Type u_8
inst : Norm E
inst_1 : SeminormedAddCommGroup F'
inst_2 : SeminormedAddCommGroup G'
f : α → E
g' : α → F'
k' : α → G'
l : Filter α
h : g' =Θ[l] k'
⊢ f =O[l] g' ↔ f =O[l] k'

Tactic:
⟨fun H ↦ H.trans_isTheta h, fun H ↦ H.trans_isTheta h.symm⟩

Premises used: Asymptotics.IsTheta.symm, Iff.intro, Asymptotics.IsBigO.trans_isTheta
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
G : Type u_5
E' : Type u_6
F' : Type u_7
inst : Norm G
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
k : α → G
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ f' =Θ[l] k ↔ g' =Θ[l] k

Tactic:
h.isBigO_congr_left.and h.isBigO_congr_right

Premises used: Asymptotics.IsTheta.isBigO_congr_left, Asymptotics.IsTheta, Iff.and, Asymptotics.IsTheta.isBigO_congr_right
-- Module: Mathlib.Analysis.Asymptotics.Theta
Goal:
α : Type u_1
G : Type u_5
E' : Type u_6
F' : Type u_7
inst : Norm G
inst_1 : SeminormedAddCommGroup E'
inst_2 : SeminormedAddCommGroup F'
k : α → G
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ k =Θ[l] f' ↔ k =Θ[l] g'

Tactic:
h.isBigO_congr_right.and h.isBigO_congr_left

Premises used: Asymptotics.IsTheta.isBigO_congr_left, Asymptotics.IsTheta, Iff.and, Asymptotics.IsTheta.isBigO_congr_right