[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
inst✝¹ : AddZeroClass β
inst✝ : ContinuousAdd β
l : Filter α
f g : α → β
hf : ZeroAtFilter l f
hg : ZeroAtFilter l g
⊢ ZeroAtFilter l (f + g)
[PROOFSTEP]
simpa using hf.add hg
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : ContinuousNeg β
l : Filter α
f : α → β
hf : ZeroAtFilter l f
⊢ ZeroAtFilter l (-f)
[PROOFSTEP]
simpa using hf.neg
[GOAL]
α : Type u_1
β : Type u_2
𝕜 : Type u_3
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMulWithZero 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
l : Filter α
f : α → β
c : 𝕜
hf : ZeroAtFilter l f
⊢ ZeroAtFilter l (c • f)
[PROOFSTEP]
simpa using hf.const_smul c
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : ZeroAtFilter l f
⊢ BoundedAtFilter l f
[PROOFSTEP]
rw [ZeroAtFilter, ← Asymptotics.isLittleO_const_iff (one_ne_zero' ℝ)] at hf 
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : f =o[l] fun _x => 1
⊢ BoundedAtFilter l f
[PROOFSTEP]
exact hf.isBigO
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ BoundedAtFilter l (f + g)
[PROOFSTEP]
simpa using hf.add hg
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ BoundedAtFilter l (f * g)
[PROOFSTEP]
refine' (hf.mul hg).trans _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
⊢ (fun x => OfNat.ofNat 1 x * OfNat.ofNat 1 x) =O[l] 1
[PROOFSTEP]
convert Asymptotics.isBigO_refl (E := ℝ) _ l
[GOAL]
case h.e'_8.h
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : BoundedAtFilter l f
hg : BoundedAtFilter l g
x✝ : α
⊢ OfNat.ofNat 1 x✝ = OfNat.ofNat 1 x✝ * OfNat.ofNat 1 x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
⊢ Subalgebra β (α → β)
[PROOFSTEP]
refine' Submodule.toSubalgebra (boundedFilterSubmodule l) _ fun f g hf hg ↦ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
⊢ 1 ∈ boundedFilterSubmodule l
[PROOFSTEP]
exact const_boundedAtFilter l (1 : β)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
l : Filter α
f g : α → β
hf : f ∈ boundedFilterSubmodule l
hg : g ∈ boundedFilterSubmodule l
⊢ f * g ∈ boundedFilterSubmodule l
[PROOFSTEP]
simpa only [Pi.one_apply, mul_one, norm_mul] using hf.mul hg
