English
For HasFPowerSeriesWithinOnBall hf, the difference f(y)−f(z)−p(1)(y−z) is bounded by a constant times max norms times the distance, uniformly on small balls in the product space near (x,x).
Русский
Для HasFPowerSeriesWithinOnBall hf разность f(y)−f(z)−p(1)(y−z) ограничена константой, пропорциональной максимуму норм и расстоянию ‖y−z‖, равномерно на малых шарах в произведении пространства около (x,x).
LaTeX
$$$\\exists C,\\; \\forall (y,z)\\in (\\mathrm{insert}\,x\,s) \\times (\\mathrm{insert}\,x\,s) \\cap \\mathrm{EMetric.ball}( (x,x), r'):\\; \\|f(y) - f(z) - p(1)(y-z)\\| \\le C \\cdot \\max\\|y-x\\| \\|z-x\\| \\cdot \\|y-z\\|$$$
Lean4
/-- If `f` has formal power series `∑ n, pₙ` in a set, within a ball of radius `r`, then
for `y, z` in any smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is
bounded above by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. This lemma formulates this property
using `IsBigO` and `Filter.principal` on `E × E`. -/
theorem isBigO_image_sub_image_sub_deriv_principal (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
(fun y : E × E =>
f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) =O[𝓟 (EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)))]
fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ :=
by
lift r' to ℝ≥0 using ne_top_of_lt hr
rcases (zero_le r').eq_or_lt with (rfl | hr'0)
· simp only [ENNReal.coe_zero, EMetric.ball_zero, empty_inter, principal_empty, isBigO_bot]
obtain ⟨a, ha, C, hC : 0 < C, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n : ℕ, ‖p n‖ * (r' : ℝ) ^ n ≤ C * a ^ n :=
p.norm_mul_pow_le_mul_pow_of_lt_radius (hr.trans_le hf.r_le)
simp only [← le_div_iff₀ (pow_pos (NNReal.coe_pos.2 hr'0) _)] at hp
set L : E × E → ℝ := fun y => C * (a / r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
have hL :
∀ y ∈ EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)), ‖f y.1 - f y.2 - p 1 fun _ => y.1 - y.2‖ ≤ L y :=
by
intro y ⟨hy', ys⟩
have hy : y ∈ EMetric.ball x r ×ˢ EMetric.ball x r :=
by
rw [EMetric.ball_prod_same]
exact EMetric.ball_subset_ball hr.le hy'
set A : ℕ → F := fun n => (p n fun _ => y.1 - x) - p n fun _ => y.2 - x
have hA : HasSum (fun n => A (n + 2)) (f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) :=
by
convert (hasSum_nat_add_iff' 2).2 ((hf.hasSum_sub ⟨ys.1, hy.1⟩).sub (hf.hasSum_sub ⟨ys.2, hy.2⟩)) using 1
rw [Finset.sum_range_succ, Finset.sum_range_one, hf.coeff_zero, hf.coeff_zero, sub_self, zero_add, ←
Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x),
Pi.single, ← (p 1).map_update_sub, ← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]
rw [EMetric.mem_ball, edist_eq_enorm_sub, enorm_lt_coe] at hy'
set B : ℕ → ℝ := fun n => C * (a / r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((n + 2) * a ^ n)
have hAB : ∀ n, ‖A (n + 2)‖ ≤ B n := fun n =>
calc
‖A (n + 2)‖ ≤ ‖p (n + 2)‖ * ↑(n + 2) * ‖y - (x, x)‖ ^ (n + 1) * ‖y.1 - y.2‖ := by
simpa only [Fintype.card_fin, pi_norm_const, Prod.norm_def, Pi.sub_def, Prod.fst_sub, Prod.snd_sub,
sub_sub_sub_cancel_right] using (p <| n + 2).norm_image_sub_le (fun _ => y.1 - x) fun _ => y.2 - x
_ = ‖p (n + 2)‖ * ‖y - (x, x)‖ ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) :=
by
rw [pow_succ ‖y - (x, x)‖]
ring
_ ≤ C * a ^ (n + 2) / r' ^ (n + 2) * r' ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) :=
by
have : 0 < a := ha.1
gcongr
· apply hp
· apply hy'.le
_ = B n := by simp [field, B, pow_succ]
have hBL : HasSum B (L y) := by
apply HasSum.mul_left
simp only [add_mul]
have : ‖a‖ < 1 := by simp only [Real.norm_eq_abs, abs_of_pos ha.1, ha.2]
rw [div_eq_mul_inv, div_eq_mul_inv]
exact (hasSum_coe_mul_geometric_of_norm_lt_one this).add ((hasSum_geometric_of_norm_lt_one this).mul_left 2)
exact hA.norm_le_of_bounded hBL hAB
suffices L =O[𝓟 (EMetric.ball (x, x) r' ∩ ((insert x s) ×ˢ (insert x s)))] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ from
.trans (.of_norm_eventuallyLE (eventually_principal.2 hL)) this
simp_rw [L, mul_right_comm _ (_ * _)]
exact (isBigO_refl _ _).const_mul_left _
