Skip to content

Commit b8947ef

Browse files
YaelDilliesYaelDillies
committed
chore: use ‖x‖ₑ instead of ↑‖x‖₊ 
1 parent a6e1dfd commit b8947ef

57 files changed

Lines changed: 869 additions & 906 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Mathlib/Analysis/Analytic/Basic.lean‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -502,13 +502,13 @@ theorem HasFPowerSeriesOnBall.comp_sub (hf : HasFPowerSeriesOnBall f p x r) (y :
502502
theorem HasFPowerSeriesWithinOnBall.hasSum_sub (hf : HasFPowerSeriesWithinOnBall f p s x r) {y : E}
503503
(hy : y ∈ (insert x s) ∩ EMetric.ball x r) :
504504
HasSum (fun n : ℕ => p n fun _ => y - x) (f y) := by
505-
have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_coe_nnnorm_sub] using hy.2
505+
have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_enorm_sub] using hy.2
506506
have := hf.hasSum (by simpa only [add_sub_cancel] using hy.1) this
507507
simpa only [add_sub_cancel]
508508

509509
theorem HasFPowerSeriesOnBall.hasSum_sub (hf : HasFPowerSeriesOnBall f p x r) {y : E}
510510
(hy : y ∈ EMetric.ball x r) : HasSum (fun n : ℕ => p n fun _ => y - x) (f y) := by
511-
have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_coe_nnnorm_sub] using hy
511+
have : y - x ∈ EMetric.ball (0 : E) r := by simpa [edist_eq_enorm_sub] using hy
512512
simpa only [add_sub_cancel] using hf.hasSum this
513513

514514
theorem HasFPowerSeriesOnBall.radius_pos (hf : HasFPowerSeriesOnBall f p x r) : 0 < p.radius :=
@@ -543,7 +543,7 @@ lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSe
543543
· simpa using h''
544544
· apply h'
545545
refine ⟨hy, ?_⟩
546-
simpa [edist_eq_coe_nnnorm_sub] using h'y
546+
simpa [edist_eq_enorm_sub] using h'y
547547

548548
/-- Variant of `HasFPowerSeriesWithinOnBall.congr` in which one requests equality on `insert x s`
549549
instead of separating `x` and `s`. -/
@@ -553,7 +553,7 @@ lemma HasFPowerSeriesWithinOnBall.congr' {f g : E → F} {p : FormalMultilinearS
553553
HasFPowerSeriesWithinOnBall g p s x r := by
554554
refine ⟨h.r_le, h.r_pos, fun {y} hy h'y ↦ ?_⟩
555555
convert h.hasSum hy h'y using 1
556-
exact h' ⟨hy, by simpa [edist_eq_coe_nnnorm_sub] using h'y⟩
556+
exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩
557557

558558
lemma HasFPowerSeriesWithinAt.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
559559
{x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) :
@@ -575,7 +575,7 @@ theorem HasFPowerSeriesOnBall.congr (hf : HasFPowerSeriesOnBall f p x r)
575575
hasSum := fun {y} hy => by
576576
convert hf.hasSum hy using 1
577577
apply hg.symm
578-
simpa [edist_eq_coe_nnnorm_sub] using hy }
578+
simpa [edist_eq_enorm_sub] using hy }
579579

580580
theorem HasFPowerSeriesAt.congr (hf : HasFPowerSeriesAt f p x) (hg : f =ᶠ[𝓝 x] g) :
581581
HasFPowerSeriesAt g p x := by
@@ -678,7 +678,7 @@ theorem HasFPowerSeriesWithinAt.mono_of_mem_nhdsWithin
678678
rcases hy with rfl | hy
679679
· simp
680680
apply mem_insert_of_mem _ (hr' ?_)
681-
simp only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, sub_zero, lt_min_iff, mem_inter_iff,
681+
simp only [EMetric.mem_ball, edist_eq_enorm_sub, sub_zero, lt_min_iff, mem_inter_iff,
682682
add_sub_cancel_left, hy, and_true] at h'y ⊢
683683
exact h'y.2
684684

@@ -911,7 +911,7 @@ theorem HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod {y : E}
911911
(atTop ×ˢ 𝓝 y) (𝓝 0) by simpa using A.add this
912912
apply Metric.tendsto_nhds.2 (fun ε εpos ↦ ?_)
913913
obtain ⟨r', yr', r'r⟩ : ∃ (r' : ℝ≥0), ‖y‖₊ < r' ∧ r' < r := by
914-
simp [edist_eq_coe_nnnorm] at hy
914+
simp [edist_zero_eq_enorm] at hy
915915
simpa using ENNReal.lt_iff_exists_nnreal_btwn.1 hy
916916
have yr'_2 : ‖y‖ < r' := by simpa [← coe_nnnorm] using yr'
917917
have S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n := p.summable_norm_mul_pow (r'r.trans_le hf.r_le)
@@ -990,7 +990,7 @@ theorem HasFPowerSeriesWithinOnBall.uniform_geometric_approx' {r' : ℝ≥0}
990990
have hr'0 : 0 < (r' : ℝ) := (norm_nonneg _).trans_lt yr'
991991
have : y ∈ EMetric.ball (0 : E) r := by
992992
refine mem_emetric_ball_zero_iff.2 (lt_trans ?_ h)
993-
exact mod_cast yr'
993+
simpa [enorm] using yr'
994994
rw [norm_sub_rev, ← mul_div_right_comm]
995995
have ya : a * (‖y‖ / ↑r') ≤ a :=
996996
mul_le_of_le_one_right ha.1.le (div_le_one_of_le₀ yr'.le r'.coe_nonneg)
@@ -1101,7 +1101,7 @@ theorem HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal
11011101
zero_add, ← Subsingleton.pi_single_eq (0 : Fin 1) (y.1 - x), Pi.single,
11021102
← Subsingleton.pi_single_eq (0 : Fin 1) (y.2 - x), Pi.single, ← (p 1).map_update_sub,
11031103
← Pi.single, Subsingleton.pi_single_eq, sub_sub_sub_cancel_right]
1104-
rw [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, ENNReal.coe_lt_coe] at hy'
1104+
rw [EMetric.mem_ball, edist_eq_enorm_sub, enorm_lt_coe] at hy'
11051105
set B : ℕ → ℝ := fun n => C * (a / r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * ((n + 2) * a ^ n)
11061106
have hAB : ∀ n, ‖A (n + 2)‖ ≤ B n := fun n =>
11071107
calc
@@ -1281,7 +1281,7 @@ theorem HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'
12811281
· ext z
12821282
simp
12831283
· intro z
1284-
simp [edist_eq_coe_nnnorm, edist_eq_coe_nnnorm_sub]
1284+
simp [edist_zero_eq_enorm, edist_eq_enorm_sub]
12851285

12861286
/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
12871287
the partial sums of this power series on the disk of convergence, i.e., `f y`

‎Mathlib/Analysis/Analytic/CPolynomial.lean‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,7 @@ theorem HasFiniteFPowerSeriesOnBall.eq_partialSum'
278278
∀ y ∈ EMetric.ball x r, ∀ m, n ≤ m →
279279
f y = p.partialSum m (y - x) := by
280280
intro y hy m hm
281-
rw [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, ← mem_emetric_ball_zero_iff] at hy
281+
rw [EMetric.mem_ball, edist_eq_enorm_sub, ← mem_emetric_ball_zero_iff] at hy
282282
rw [← (HasFiniteFPowerSeriesOnBall.eq_partialSum hf _ hy m hm), add_sub_cancel]
283283

284284
/-! The particular cases where `f` has a finite power series bounded by `0` or `1`. -/
@@ -300,8 +300,8 @@ theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (hf : ∀ y ∈ EMetri
300300
rw [hf (x + y)]
301301
· convert hasSum_zero
302302
rw [hp, ContinuousMultilinearMap.zero_apply]
303-
· rwa [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, add_comm, add_sub_cancel_right,
304-
← edist_eq_coe_nnnorm, ← EMetric.mem_ball]
303+
· rwa [EMetric.mem_ball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
304+
← edist_zero_eq_enorm, ← EMetric.mem_ball]
305305

306306
/-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
307307
neighborhood of `x`. -/
@@ -504,8 +504,7 @@ theorem HasFiniteFPowerSeriesOnBall.changeOrigin (hf : HasFiniteFPowerSeriesOnBa
504504
FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
505505
rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
506506
rw [p.changeOrigin_eval_of_finite hf.finite, add_assoc, hf.sum]
507-
refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ hz)
508-
exact mod_cast nnnorm_add_le y z
507+
exact mem_emetric_ball_zero_iff.2 ((enorm_add_le _ _).trans_lt hz)
509508
rw [this]
510509
apply (p.changeOrigin y).hasSum_of_finite fun _ => p.changeOrigin_finite_of_finite hf.finite
511510

@@ -514,7 +513,7 @@ it is continuously polynomial at every point of this ball. -/
514513
theorem HasFiniteFPowerSeriesOnBall.cPolynomialAt_of_mem
515514
(hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : y ∈ EMetric.ball x r) :
516515
CPolynomialAt 𝕜 f y := by
517-
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h
516+
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h
518517
have := hf.changeOrigin this
519518
rw [add_sub_cancel] at this
520519
exact this.cPolynomialAt

‎Mathlib/Analysis/Analytic/ChangeOrigin.lean‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -306,8 +306,8 @@ variable [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F}
306306
it also admits a power series on any subball of this ball (even with a different center provided
307307
it belongs to `s`), given by `p.changeOrigin`. -/
308308
theorem HasFPowerSeriesWithinOnBall.changeOrigin (hf : HasFPowerSeriesWithinOnBall f p s x r)
309-
(h : (‖y‖₊ : ℝ≥0∞) < r) (hy : x + y ∈ insert x s) :
310-
HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖₊) where
309+
(h : ‖y‖ₑ < r) (hy : x + y ∈ insert x s) :
310+
HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖ₑ) where
311311
r_le := by
312312
apply le_trans _ p.changeOrigin_radius
313313
exact tsub_le_tsub hf.r_le le_rfl
@@ -322,8 +322,7 @@ theorem HasFPowerSeriesWithinOnBall.changeOrigin (hf : HasFPowerSeriesWithinOnBa
322322
rw [insert_eq_of_mem hy] at this
323323
apply this
324324
simpa [add_assoc] using h'z
325-
refine mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt ?_ hz)
326-
exact mod_cast nnnorm_add_le y z
325+
exact mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)
327326
rw [this]
328327
apply (p.changeOrigin y).hasSum
329328
refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz
@@ -342,7 +341,7 @@ it is analytic at every point of this ball. -/
342341
theorem HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem
343342
(hf : HasFPowerSeriesWithinOnBall f p s x r)
344343
(h : y ∈ insert x s ∩ EMetric.ball x r) : AnalyticWithinAt 𝕜 f s y := by
345-
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_coe_nnnorm_sub] using h.2
344+
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h.2
346345
have := hf.changeOrigin this (by simpa using h.1)
347346
rw [add_sub_cancel] at this
348347
exact this.analyticWithinAt

‎Mathlib/Analysis/Analytic/Composition.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -742,7 +742,7 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
742742
apply hδ
743743
have : y ∈ EMetric.ball (0 : E) δ :=
744744
(EMetric.ball_subset_ball (le_trans (min_le_left _ _) (min_le_right _ _))) hy
745-
simpa [-Set.mem_insert_iff, edist_eq_coe_nnnorm_sub, h'y]
745+
simpa [-Set.mem_insert_iff, edist_eq_enorm_sub, h'y]
746746
/- Now the proof starts. To show that the sum of `q.comp p` at `y` is `g (f (x + y))`,
747747
we will write `q.comp p` applied to `y` as a big sum over all compositions.
748748
Since the sum is summable, to get its convergence it suffices to get
@@ -775,7 +775,7 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
775775
have : Tendsto (fun (z : ℕ × F) ↦ q.partialSum z.1 z.2)
776776
(atTop ×ˢ 𝓝 (f (x + y) - f x)) (𝓝 (g (f x + (f (x + y) - f x)))) := by
777777
apply Hg.tendsto_partialSum_prod (y := f (x + y) - f x)
778-
· simpa [edist_eq_coe_nnnorm_sub] using fy_mem.2
778+
· simpa [edist_eq_enorm_sub] using fy_mem.2
779779
· simpa using fy_mem.1
780780
simpa using this.comp A
781781
-- Third step: the sum over all compositions in `compPartialSumTarget 0 n n` converges to
@@ -806,9 +806,9 @@ theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMult
806806
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
807807
rw [Finset.prod_const, Finset.card_fin]
808808
gcongr
809-
rw [EMetric.mem_ball, edist_eq_coe_nnnorm] at hy
809+
rw [EMetric.mem_ball, edist_zero_eq_enorm] at hy
810810
have := le_trans (le_of_lt hy) (min_le_right _ _)
811-
rwa [ENNReal.coe_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
811+
rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
812812
tendsto_nhds_of_cauchySeq_of_subseq cau compPartialSumTarget_tendsto_atTop C
813813
-- Fifth step: the sum over `n` of `q.comp p n` can be expressed as a particular resummation of
814814
-- the sum over all compositions, by grouping together the compositions of the same

‎Mathlib/Analysis/Analytic/Inverse.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -592,9 +592,9 @@ lemma HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp
592592
apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
593593
rw [Finset.prod_const, Finset.card_fin]
594594
gcongr
595-
rw [EMetric.mem_ball, edist_eq_coe_nnnorm] at hy
595+
rw [EMetric.mem_ball, edist_zero_eq_enorm] at hy
596596
have := le_trans (le_of_lt hy) (min_le_right _ _)
597-
rwa [ENNReal.coe_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
597+
rwa [enorm_le_coe, ← NNReal.coe_le_coe, coe_nnnorm] at this
598598
apply HasSum.of_sigma (fun b ↦ hasSum_fintype _) ?_ cau
599599
simpa [FormalMultilinearSeries.comp] using h0.hasSum hy0
600600
have B : Tendsto (fun (n : ℕ × ℕ) => ∑ i ∈ compPartialSumTarget 0 n.1 n.2,
@@ -686,7 +686,7 @@ theorem PartialHomeomorph.hasFPowerSeriesAt_symm (f : PartialHomeomorph E F) {a
686686
refine ⟨min r (p.leftInv i a).radius, min_le_right _ _,
687687
lt_min r_pos (radius_leftInv_pos_of_radius_pos h.radius_pos hp), fun {y} hy ↦ ?_⟩
688688
have : y + f a ∈ EMetric.ball (f a) r := by
689-
simp only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, sub_zero, lt_min_iff,
689+
simp only [EMetric.mem_ball, edist_eq_enorm_sub, sub_zero, lt_min_iff,
690690
add_sub_cancel_right] at hy ⊢
691691
exact hy.1
692692
simpa [add_comm] using hr this

‎Mathlib/Analysis/Analytic/Uniqueness.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f
183183
EMetric.mem_closure_iff.1 xu (r / 2) (ENNReal.half_pos hp.r_pos.ne')
184184
let q := p.changeOrigin (y - x)
185185
have has_series : HasFPowerSeriesOnBall f q y (r / 2) := by
186-
have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_coe_nnnorm_sub] at hxy
186+
have A : (‖y - x‖₊ : ℝ≥0∞) < r / 2 := by rwa [edist_comm, edist_eq_enorm_sub] at hxy
187187
have := hp.changeOrigin (A.trans_le ENNReal.half_le_self)
188188
simp only [add_sub_cancel] at this
189189
apply this.mono (ENNReal.half_pos hp.r_pos.ne')

‎Mathlib/Analysis/Analytic/Within.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -124,14 +124,14 @@ lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpac
124124
· intro h
125125
refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
126126
· intro y ⟨ys,yb⟩
127-
simp only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub] at yb
127+
simp only [EMetric.mem_ball, edist_eq_enorm_sub] at yb
128128
have e0 := p.hasSum (x := y - x) ?_
129129
have e1 := (h.hasSum (y := y - x) ?_ ?_)
130130
· simp only [add_sub_cancel] at e1
131131
exact e1.unique e0
132132
· simpa only [add_sub_cancel]
133-
· simpa only [EMetric.mem_ball, edist_eq_coe_nnnorm]
134-
· simp only [EMetric.mem_ball, edist_eq_coe_nnnorm]
133+
· simpa only [EMetric.mem_ball, edist_zero_eq_enorm]
134+
· simp only [EMetric.mem_ball, edist_zero_eq_enorm]
135135
exact lt_of_lt_of_le yb h.r_le
136136
· refine ⟨h.r_le, h.r_pos, ?_⟩
137137
intro y lt
@@ -145,7 +145,7 @@ lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpac
145145
rw [hfg]
146146
· exact hg.hasSum lt
147147
· refine ⟨ys, ?_⟩
148-
simpa only [EMetric.mem_ball, edist_eq_coe_nnnorm_sub, add_sub_cancel_left, sub_zero] using lt
148+
simpa only [EMetric.mem_ball, edist_eq_enorm_sub, add_sub_cancel_left, sub_zero] using lt
149149

150150
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series -/
151151
lemma hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt [CompleteSpace F] {f : E → F}

‎Mathlib/Analysis/BoxIntegral/Integrability.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,7 @@ theorem IntegrableOn.hasBoxIntegral [CompleteSpace E] {f : (ι → ℝ) → E} {
223223
-- Choose `N` such that the integral of `‖f N x - g x‖` is less than or equal to `ε`.
224224
obtain ⟨N₀, hN₀⟩ : ∃ N : ℕ, ∫ x in I, ‖f N x - g x‖ ∂μ ≤ ε := by
225225
have : Tendsto (fun n => ∫⁻ x in I, ‖f n x - g x‖₊ ∂μ) atTop (𝓝 0) :=
226-
SimpleFunc.tendsto_approxOn_range_L1_nnnorm hg.measurable hgi
226+
SimpleFunc.tendsto_approxOn_range_L1_enorm hg.measurable hgi
227227
refine (this.eventually (ge_mem_nhds ε0')).exists.imp fun N hN => ?_
228228
exact integral_coe_le_of_lintegral_coe_le hN
229229
-- For each `x`, we choose `Nx x ≥ N₀` such that `dist (f Nx x) (g x) ≤ ε`.

‎Mathlib/Analysis/Calculus/FDeriv/Analytic.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,7 @@ protected theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F]
204204
(h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x
205205
dsimp only
206206
rw [← h.fderiv_eq, add_sub_cancel]
207-
simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
207+
simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz
208208

209209
/-- If a function has a power series within a set on a ball, then so does its derivative. -/
210210
protected theorem HasFPowerSeriesWithinOnBall.fderivWithin [CompleteSpace F]
@@ -219,7 +219,7 @@ protected theorem HasFPowerSeriesWithinOnBall.fderivWithin [CompleteSpace F]
219219
(h.r_pos.trans_le h.r_le)).mono h.r_pos h.r_le).comp_sub x
220220
· dsimp only
221221
rw [← h.fderivWithin_eq _ _ hu, add_sub_cancel]
222-
· simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz.2
222+
· simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz.2
223223
· simpa using hz.1
224224

225225
/-- If a function has a power series within a set on a ball, then so does its derivative. For a
@@ -313,7 +313,7 @@ theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
313313
rw [← b.isEmbedding.hasSum_iff]
314314
have : HasFPowerSeriesWithinOnBall (a ∘ f) (a.compFormalMultilinearSeries p) s x r :=
315315
a.comp_hasFPowerSeriesWithinOnBall h
316-
have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_eq_coe_nnnorm] using hy)
316+
have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_zero_eq_enorm] using hy)
317317
have : fderivWithin 𝕜 (a ∘ f) (insert x s) (x + y) = a ∘L f' := by
318318
apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)
319319
exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'
@@ -337,7 +337,7 @@ protected theorem HasFPowerSeriesWithinOnBall.fderivWithin_of_mem_of_analyticOn
337337
(h : AnalyticOn 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
338338
HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f s) p.derivSeries s x r := by
339339
refine ⟨hr.r_le.trans p.radius_le_radius_derivSeries, hr.r_pos, fun {y} hy h'y ↦ ?_⟩
340-
apply hr.hasSum_derivSeries_of_hasFDerivWithinAt (by simpa [edist_eq_coe_nnnorm] using h'y) hy
340+
apply hr.hasSum_derivSeries_of_hasFDerivWithinAt (by simpa [edist_zero_eq_enorm] using h'y) hy
341341
· rw [insert_eq_of_mem hx] at hy ⊢
342342
apply DifferentiableWithinAt.hasFDerivWithinAt
343343
exact h.differentiableOn _ hy
@@ -487,7 +487,7 @@ protected theorem HasFiniteFPowerSeriesOnBall.fderiv
487487
((p.hasFiniteFPowerSeriesOnBall_changeOrigin 1 h.finite).mono h.r_pos le_top).comp_sub x
488488
dsimp only
489489
rw [← h.fderiv_eq, add_sub_cancel]
490-
simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz
490+
simpa only [edist_eq_enorm_sub, EMetric.mem_ball] using hz
491491

492492
/-- If a function has a finite power series on a ball, then so does its derivative.
493493
This is a variant of `HasFiniteFPowerSeriesOnBall.fderiv` where the degree of `f` is `< n`

‎Mathlib/Analysis/Complex/CauchyIntegral.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -536,7 +536,7 @@ theorem hasFPowerSeriesOnBall_of_differentiable_off_countable {R : ℝ≥0} {c :
536536
hasSum := fun {w} hw => by
537537
have hw' : c + w ∈ ball c R := by
538538
simpa only [add_mem_ball_iff_norm, ← coe_nnnorm, mem_emetric_ball_zero_iff,
539-
NNReal.coe_lt_coe, ENNReal.coe_lt_coe] using hw
539+
NNReal.coe_lt_coe, enorm_lt_coe] using hw
540540
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
541541
hs hw' hc hd]
542542
exact (hasFPowerSeriesOn_cauchy_integral

0 commit comments

Comments
 (0)