English
If f and g are IsRestricted with parameter c (over an ultrametric dist space), then f*g is IsRestricted with the same c.
Русский
Если f и g ограничены по c в пространстве с ультраметрическим расстоянием, то произведение f*g ограничено по c.
LaTeX
$$$\text{IsRestricted}(c,f) \land \text{IsRestricted}(c,g) \Rightarrow \text{IsRestricted}(c, f*g)$$$
Lean4
theorem mul {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f * g) :=
by
obtain ⟨a, ha, fBound1⟩ :=
(bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ ((isRestricted_iff_abs c f).mp hf))
obtain ⟨b, hb, gBound1⟩ :=
(bddAbove_iff_exists_ge 1).mp (convergenceSet_BddAbove _ ((isRestricted_iff_abs c g).mp hg))
simp only [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at fBound1 gBound1
simp only [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm, PowerSeries.coeff_mul] at ⊢ hf hg
intro ε hε
obtain ⟨Nf, fBound2⟩ := (hf (ε / (max a b))) (by positivity)
obtain ⟨Ng, gBound2⟩ := (hg (ε / (max a b))) (by positivity)
refine ⟨2 * max Nf Ng, fun n hn ↦ ?_⟩
obtain ⟨⟨fst, snd⟩, hi, ultrametric⟩ :=
exists_norm_finset_sum_le (Finset.antidiagonal n) (fun a ↦ (coeff a.1) f * (coeff a.2) g)
obtain ⟨rfl⟩ := by simpa using hi (⟨(0, n), by simp⟩)
calc
_ ≤ ‖(coeff fst) f * (coeff snd) g‖ * |c| ^ (fst + snd) := by bound
_ ≤ ‖(coeff fst) f‖ * |c| ^ fst * (‖(coeff snd) g‖ * |c| ^ snd) := by grw [norm_mul_le]; grind
have : max Nf Ng ≤ fst ∨ max Nf Ng ≤ snd := by omega
rcases this with this | this
·
calc
_ < ε / max a b * b := by
grw [gBound1 snd]
gcongr
exact fBound2 fst (by omega)
_ ≤ ε := by
rw [div_mul_comm, mul_le_iff_le_one_left ‹_›]
bound
·
calc
_ < a * (ε / max a b) := by
grw [fBound1 fst]
gcongr
exact gBound2 snd (by omega)
_ ≤ ε := by
rw [mul_div_left_comm, mul_le_iff_le_one_right ‹_›]
bound
