-- Mathlib/Analysis/Analytic/Constructions.lean
/-- The radius of the Cartesian product of two formal series is the minimum of their radii. -/
lemma FormalMultilinearSeries.radius_prod_eq_min
    (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) :
    (p.prod q).radius = min p.radius q.radius

Proof state:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
⊢ ↑r ≤ (p.prod q).radius

Tactic:
have := ((p.isLittleO_one_of_lt_radius hr.1).add
  (q.isLittleO_one_of_lt_radius hr.2)).isBigO

Result:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1
⊢ ↑r ≤ (p.prod q).radius

Proof state:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ⊓ q.radius
⊢ ↑r ≤ (p.prod q).radius

Tactic:
rw [lt_min_iff] at hr

Result:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
⊢ ↑r ≤ (p.prod q).radius

Proof state:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1
⊢ ↑r ≤ (p.prod q).radius

Tactic:
refine (p.prod q).le_radius_of_isBigO ((isBigO_of_le _ fun n ↦ ?_).trans this)

Result:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1
n : ℕ
⊢ ‖‖p.prod q n‖ * ↑r ^ n‖ ≤ ‖‖p n‖ * ↑r ^ n + ‖q n‖ * ↑r ^ n‖

Proof state:
case a.right.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n => ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x => 1
n : ℕ
⊢ ‖q n‖ ≤ ‖p n‖ ⊔ ‖q n‖

Tactic:
apply le_max_right

Result:
no goals

Proof state:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
⊢ ↑r ≤ p.radius ⊓ q.radius

Tactic:
rw [le_min_iff]

Result:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
⊢ ↑r ≤ p.radius ∧ ↑r ≤ q.radius

Proof state:
case a.right.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n => ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x => 1
n : ℕ
⊢ ‖q n‖ ≤ ‖p.prod q n‖

Tactic:
rw [FormalMultilinearSeries.prod, ContinuousMultilinearMap.opNorm_prod]

Result:
case a.right.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n => ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x => 1
n : ℕ
⊢ ‖q n‖ ≤ ‖p n‖ ⊔ ‖q n‖

Proof state:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1
n : ℕ
⊢ ‖p n‖ ⊔ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_

Result:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x => ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x => 1
n : ℕ
⊢ ‖p n‖ + ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Proof state:
case a.left.h
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < (p.prod q).radius
this : (fun n => ‖p.prod q n‖ * ↑r ^ n) =o[atTop] fun x => 1
n : ℕ
⊢ ‖p n‖ ≤ ‖p n‖ ⊔ ‖q n‖

Tactic:
apply le_max_left

Result:
no goals