Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 839b92f

Browse files
urkudurkud
committed
feat(data/nat/enat): new file (#16217)
Define `enat := with_top nat`, use notation.
1 parent 474f96a commit 839b92f

34 files changed

Lines changed: 253 additions & 207 deletions

‎src/algebra/group/to_additive.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -411,7 +411,7 @@ There are some exceptions to this heuristic:
411411
* If an identifier has attribute `@[to_additive_ignore_args n1 n2 ...]` then all the arguments in
412412
positions `n1`, `n2`, ... will not be checked for unapplied identifiers (start counting from 1).
413413
For example, `cont_mdiff_map` has attribute `@[to_additive_ignore_args 21]`, which means
414-
that its 21st argument `(n : with_top ℕ)` can contain `ℕ`
414+
that its 21st argument `(n : ℕ∞)` can contain `ℕ`
415415
(usually in the form `has_top.top ℕ ...`) and still be additivized.
416416
So `@has_mul.mul (C^∞⟮I, N; I', G⟯) _ f g` will be additivized.
417417

‎src/analysis/calculus/affine_map.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ variables [normed_add_comm_group V] [normed_space 𝕜 V]
2424
variables [normed_add_comm_group W] [normed_space 𝕜 W]
2525

2626
/-- A continuous affine map between normed vector spaces is smooth. -/
27-
lemma cont_diff {n : with_top ℕ} (f : V →A[𝕜] W) :
27+
lemma cont_diff {n : ℕ∞} (f : V →A[𝕜] W) :
2828
cont_diff 𝕜 n f :=
2929
begin
3030
rw f.decomp,

‎src/analysis/calculus/cont_diff.lean‎

Lines changed: 57 additions & 56 deletions
Large diffs are not rendered by default.

‎src/analysis/calculus/fderiv_analytic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ begin
121121
end
122122

123123
/-- An analytic function is infinitely differentiable. -/
124-
lemma analytic_on.cont_diff_on [complete_space F] (h : analytic_on 𝕜 f s) {n : with_top ℕ} :
124+
lemma analytic_on.cont_diff_on [complete_space F] (h : analytic_on 𝕜 f s) {n : ℕ∞} :
125125
cont_diff_on 𝕜 n f s :=
126126
begin
127127
let t := {x | analytic_at 𝕜 f x},

‎src/analysis/calculus/inverse.lean‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -732,40 +732,40 @@ variables [complete_space E'] (f : E' → F') {f' : E' ≃L[𝕂] F'} {a : E'}
732732
/-- Given a `cont_diff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible
733733
derivative at `a`, returns a `local_homeomorph` with `to_fun = f` and `a ∈ source`. -/
734734
def to_local_homeomorph
735-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
735+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
736736
(hn : 1 ≤ n) :
737737
local_homeomorph E' F' :=
738738
(hf.has_strict_fderiv_at' hf' hn).to_local_homeomorph f
739739

740740
variable {f}
741741

742742
@[simp] lemma to_local_homeomorph_coe
743-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
743+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
744744
(hn : 1 ≤ n) :
745745
(hf.to_local_homeomorph f hf' hn : E' → F') = f := rfl
746746

747747
lemma mem_to_local_homeomorph_source
748-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
748+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
749749
(hn : 1 ≤ n) :
750750
a ∈ (hf.to_local_homeomorph f hf' hn).source :=
751751
(hf.has_strict_fderiv_at' hf' hn).mem_to_local_homeomorph_source
752752

753753
lemma image_mem_to_local_homeomorph_target
754-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
754+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
755755
(hn : 1 ≤ n) :
756756
f a ∈ (hf.to_local_homeomorph f hf' hn).target :=
757757
(hf.has_strict_fderiv_at' hf' hn).image_mem_to_local_homeomorph_target
758758

759759
/-- Given a `cont_diff` function over `𝕂` (which is `ℝ` or `ℂ`) with an invertible derivative
760760
at `a`, returns a function that is locally inverse to `f`. -/
761761
def local_inverse
762-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
762+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
763763
(hn : 1 ≤ n) :
764764
F' → E' :=
765765
(hf.has_strict_fderiv_at' hf' hn).local_inverse f f' a
766766

767767
lemma local_inverse_apply_image
768-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
768+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
769769
(hn : 1 ≤ n) :
770770
hf.local_inverse hf' hn (f a) = a :=
771771
(hf.has_strict_fderiv_at' hf' hn).local_inverse_apply_image
@@ -774,7 +774,7 @@ lemma local_inverse_apply_image
774774
at `a`, the inverse function (produced by `cont_diff.to_local_homeomorph`) is
775775
also `cont_diff`. -/
776776
lemma to_local_inverse
777-
{n : with_top ℕ} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
777+
{n : ℕ∞} (hf : cont_diff_at 𝕂 n f a) (hf' : has_fderiv_at f (f' : E' →L[𝕂] F') a)
778778
(hn : 1 ≤ n) :
779779
cont_diff_at 𝕂 n (hf.local_inverse hf' hn) (f a) :=
780780
begin

‎src/analysis/calculus/iterated_deriv.lean‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -108,10 +108,10 @@ by { simp [iterated_deriv_within, iterated_fderiv_within_one_apply hs hx], refl
108108
derivatives are differentiable, then the function is `C^n`. This is not an equivalence in general,
109109
but this is an equivalence when the set has unique derivatives, see
110110
`cont_diff_on_iff_continuous_on_differentiable_on_deriv`. -/
111-
lemma cont_diff_on_of_continuous_on_differentiable_on_deriv {n : with_top ℕ}
112-
(Hcont : ∀ (m : ℕ), (m : with_top ℕ) ≤ n →
111+
lemma cont_diff_on_of_continuous_on_differentiable_on_deriv {n : ℕ∞}
112+
(Hcont : ∀ (m : ℕ), (m : ℕ∞) ≤ n →
113113
continuous_on (λ x, iterated_deriv_within m f s x) s)
114-
(Hdiff : ∀ (m : ℕ), (m : with_top ℕ) < n →
114+
(Hdiff : ∀ (m : ℕ), (m : ℕ∞) < n →
115115
differentiable_on 𝕜 (λ x, iterated_deriv_within m f s x) s) :
116116
cont_diff_on 𝕜 n f s :=
117117
begin
@@ -125,8 +125,8 @@ first `n` derivatives are differentiable. This is slightly too strong as the con
125125
require on the `n`-th derivative is differentiability instead of continuity, but it has the
126126
advantage of avoiding the discussion of continuity in the proof (and for `n = ∞` this is optimal).
127127
-/
128-
lemma cont_diff_on_of_differentiable_on_deriv {n : with_top ℕ}
129-
(h : ∀(m : ℕ), (m : with_top ℕ) ≤ n → differentiable_on 𝕜 (iterated_deriv_within m f s) s) :
128+
lemma cont_diff_on_of_differentiable_on_deriv {n : ℕ∞}
129+
(h : ∀(m : ℕ), (m : ℕ∞) ≤ n → differentiable_on 𝕜 (iterated_deriv_within m f s) s) :
130130
cont_diff_on 𝕜 n f s :=
131131
begin
132132
apply cont_diff_on_of_differentiable_on,
@@ -136,28 +136,28 @@ end
136136

137137
/-- On a set with unique derivatives, a `C^n` function has derivatives up to `n` which are
138138
continuous. -/
139-
lemma cont_diff_on.continuous_on_iterated_deriv_within {n : with_top ℕ} {m : ℕ}
140-
(h : cont_diff_on 𝕜 n f s) (hmn : (m : with_top ℕ) ≤ n) (hs : unique_diff_on 𝕜 s) :
139+
lemma cont_diff_on.continuous_on_iterated_deriv_within {n : ℕ∞} {m : ℕ}
140+
(h : cont_diff_on 𝕜 n f s) (hmn : (m : ℕ∞) ≤ n) (hs : unique_diff_on 𝕜 s) :
141141
continuous_on (iterated_deriv_within m f s) s :=
142142
by simpa only [iterated_deriv_within_eq_equiv_comp, linear_isometry_equiv.comp_continuous_on_iff]
143143
using h.continuous_on_iterated_fderiv_within hmn hs
144144

145145
/-- On a set with unique derivatives, a `C^n` function has derivatives less than `n` which are
146146
differentiable. -/
147-
lemma cont_diff_on.differentiable_on_iterated_deriv_within {n : with_top ℕ} {m : ℕ}
148-
(h : cont_diff_on 𝕜 n f s) (hmn : (m : with_top ℕ) < n) (hs : unique_diff_on 𝕜 s) :
147+
lemma cont_diff_on.differentiable_on_iterated_deriv_within {n : ℕ∞} {m : ℕ}
148+
(h : cont_diff_on 𝕜 n f s) (hmn : (m : ℕ∞) < n) (hs : unique_diff_on 𝕜 s) :
149149
differentiable_on 𝕜 (iterated_deriv_within m f s) s :=
150150
by simpa only [iterated_deriv_within_eq_equiv_comp,
151151
linear_isometry_equiv.comp_differentiable_on_iff]
152152
using h.differentiable_on_iterated_fderiv_within hmn hs
153153

154154
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
155155
reformulated in terms of the one-dimensional derivative on sets with unique derivatives. -/
156-
lemma cont_diff_on_iff_continuous_on_differentiable_on_deriv {n : with_top ℕ}
156+
lemma cont_diff_on_iff_continuous_on_differentiable_on_deriv {n : ℕ∞}
157157
(hs : unique_diff_on 𝕜 s) :
158158
cont_diff_on 𝕜 n f s ↔
159-
(∀m:ℕ, (m : with_top ℕ) ≤ n → continuous_on (iterated_deriv_within m f s) s)
160-
∧ (∀m:ℕ, (m : with_top ℕ) < n → differentiable_on 𝕜 (iterated_deriv_within m f s) s) :=
159+
(∀m:ℕ, (m : ℕ∞) ≤ n → continuous_on (iterated_deriv_within m f s) s)
160+
∧ (∀m:ℕ, (m : ℕ∞) < n → differentiable_on 𝕜 (iterated_deriv_within m f s) s) :=
161161
by simp only [cont_diff_on_iff_continuous_on_differentiable_on hs,
162162
iterated_fderiv_within_eq_equiv_comp, linear_isometry_equiv.comp_continuous_on_iff,
163163
linear_isometry_equiv.comp_differentiable_on_iff]
@@ -232,10 +232,10 @@ by { ext x, simp [iterated_deriv], refl }
232232

233233
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
234234
reformulated in terms of the one-dimensional derivative. -/
235-
lemma cont_diff_iff_iterated_deriv {n : with_top ℕ} :
235+
lemma cont_diff_iff_iterated_deriv {n : ℕ∞} :
236236
cont_diff 𝕜 n f ↔
237-
(∀m:ℕ, (m : with_top ℕ) ≤ n → continuous (iterated_deriv m f))
238-
∧ (∀m:ℕ, (m : with_top ℕ) < n → differentiable 𝕜 (iterated_deriv m f)) :=
237+
(∀m:ℕ, (m : ℕ∞) ≤ n → continuous (iterated_deriv m f))
238+
∧ (∀m:ℕ, (m : ℕ∞) < n → differentiable 𝕜 (iterated_deriv m f)) :=
239239
by simp only [cont_diff_iff_continuous_differentiable, iterated_fderiv_eq_equiv_comp,
240240
linear_isometry_equiv.comp_continuous_iff, linear_isometry_equiv.comp_differentiable_iff]
241241

@@ -244,19 +244,19 @@ first `n` derivatives are differentiable. This is slightly too strong as the con
244244
require on the `n`-th derivative is differentiability instead of continuity, but it has the
245245
advantage of avoiding the discussion of continuity in the proof (and for `n = ∞` this is optimal).
246246
-/
247-
lemma cont_diff_of_differentiable_iterated_deriv {n : with_top ℕ}
248-
(h : ∀(m : ℕ), (m : with_top ℕ) ≤ n → differentiable 𝕜 (iterated_deriv m f)) :
247+
lemma cont_diff_of_differentiable_iterated_deriv {n : ℕ∞}
248+
(h : ∀(m : ℕ), (m : ℕ∞) ≤ n → differentiable 𝕜 (iterated_deriv m f)) :
249249
cont_diff 𝕜 n f :=
250250
cont_diff_iff_iterated_deriv.2
251251
⟨λ m hm, (h m hm).continuous, λ m hm, (h m (le_of_lt hm))⟩
252252

253-
lemma cont_diff.continuous_iterated_deriv {n : with_top ℕ} (m : ℕ)
254-
(h : cont_diff 𝕜 n f) (hmn : (m : with_top ℕ) ≤ n) :
253+
lemma cont_diff.continuous_iterated_deriv {n : ℕ∞} (m : ℕ)
254+
(h : cont_diff 𝕜 n f) (hmn : (m : ℕ∞) ≤ n) :
255255
continuous (iterated_deriv m f) :=
256256
(cont_diff_iff_iterated_deriv.1 h).1 m hmn
257257

258-
lemma cont_diff.differentiable_iterated_deriv {n : with_top ℕ} (m : ℕ)
259-
(h : cont_diff 𝕜 n f) (hmn : (m : with_top ℕ) < n) :
258+
lemma cont_diff.differentiable_iterated_deriv {n : ℕ∞} (m : ℕ)
259+
(h : cont_diff 𝕜 n f) (hmn : (m : ℕ∞) < n) :
260260
differentiable 𝕜 (iterated_deriv m f) :=
261261
(cont_diff_iff_iterated_deriv.1 h).2 m hmn
262262

‎src/analysis/calculus/specific_functions.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -293,7 +293,7 @@ lemma R_pos {c : E} (f : cont_diff_bump_of_inner c) : 0 < f.R := f.r_pos.trans f
293293
instance (c : E) : inhabited (cont_diff_bump_of_inner c) := ⟨⟨1, 2, zero_lt_one, one_lt_two⟩⟩
294294

295295
variables [inner_product_space ℝ E] [normed_add_comm_group X] [normed_space ℝ X]
296-
variables {c : E} (f : cont_diff_bump_of_inner c) {x : E} {n : with_top ℕ}
296+
variables {c : E} (f : cont_diff_bump_of_inner c) {x : E} {n : ℕ∞}
297297

298298
/-- The function defined by `f : cont_diff_bump_of_inner c`. Use automatic coercion to
299299
function instead. -/
@@ -406,7 +406,7 @@ rfl
406406
lemma nonneg_normed (x : E) : 0 ≤ f.normed μ x :=
407407
div_nonneg f.nonneg $ integral_nonneg f.nonneg'
408408

409-
lemma cont_diff_normed {n : with_top ℕ} : cont_diff ℝ n (f.normed μ) :=
409+
lemma cont_diff_normed {n : ℕ∞} : cont_diff ℝ n (f.normed μ) :=
410410
f.cont_diff.div_const
411411

412412
lemma continuous_normed : continuous (f.normed μ) :=

‎src/analysis/complex/real_deriv.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ begin
6464
simpa using (C.comp z (B.comp z A)).has_deriv_at
6565
end
6666

67-
theorem cont_diff_at.real_of_complex {n : with_top ℕ} (h : cont_diff_at ℂ n e z) :
67+
theorem cont_diff_at.real_of_complex {n : ℕ∞} (h : cont_diff_at ℂ n e z) :
6868
cont_diff_at ℝ n (λ x : ℝ, (e x).re) z :=
6969
begin
7070
have A : cont_diff_at ℝ n (coe : ℝ → ℂ) z,
@@ -74,7 +74,7 @@ begin
7474
exact C.comp z (B.comp z A)
7575
end
7676

77-
theorem cont_diff.real_of_complex {n : with_top ℕ} (h : cont_diff ℂ n e) :
77+
theorem cont_diff.real_of_complex {n : ℕ∞} (h : cont_diff ℂ n e) :
7878
cont_diff ℝ n (λ x : ℝ, (e x).re) :=
7979
cont_diff_iff_cont_diff_at.2 $ λ x,
8080
h.cont_diff_at.real_of_complex

‎src/analysis/convolution.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -684,7 +684,7 @@ end normed_add_comm_group
684684

685685
namespace cont_diff_bump_of_inner
686686

687-
variables {n : with_top ℕ}
687+
variables {n : ℕ∞}
688688
variables [normed_space ℝ E']
689689
variables [inner_product_space ℝ G]
690690
variables [complete_space E']
@@ -758,7 +758,7 @@ variables [normed_space 𝕜 E]
758758
variables [normed_space 𝕜 E']
759759
variables [normed_space 𝕜 E'']
760760
variables [normed_space ℝ F] [normed_space 𝕜 F]
761-
variables {n : with_top ℕ}
761+
variables {n : ℕ∞}
762762
variables [complete_space F]
763763
variables [measurable_space G] {μ : measure G}
764764
variables (L : E →L[𝕜] E' →L[𝕜] F)
@@ -854,7 +854,7 @@ lemma has_compact_support.cont_diff_convolution_right [finite_dimensional 𝕜 G
854854
(hcg : has_compact_support g) (hf : locally_integrable f μ) (hg : cont_diff 𝕜 n g) :
855855
cont_diff 𝕜 n (f ⋆[L, μ] g) :=
856856
begin
857-
induction n using with_top.nat_induction with n ih ih generalizing g,
857+
induction n using enat.nat_induction with n ih ih generalizing g,
858858
{ rw [cont_diff_zero] at hg ⊢,
859859
exact hcg.continuous_convolution_right L hf hg },
860860
{ have h : ∀ x, has_fderiv_at (f ⋆[L, μ] g) ((f ⋆[L.precompR G, μ] fderiv 𝕜 g) x) x :=
@@ -888,7 +888,7 @@ variables [normed_space 𝕜 E]
888888
variables [normed_space 𝕜 E']
889889
variables [normed_space ℝ F] [normed_space 𝕜 F]
890890
variables {f₀ : 𝕜 → E} {g₀ : 𝕜 → E'}
891-
variables {n : with_top ℕ}
891+
variables {n : ℕ∞}
892892
variables (L : E →L[𝕜] E' →L[𝕜] F)
893893
variables [complete_space F]
894894
variables {μ : measure 𝕜}

‎src/analysis/inner_product_space/calculus.lean‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ lemma differentiable_inner : differentiable ℝ (λ p : E × E, ⟪p.1, p.2⟫)
5353
is_bounded_bilinear_map_inner.differentiable_at
5454

5555
variables {G : Type*} [normed_add_comm_group G] [normed_space ℝ G]
56-
{f g : G → E} {f' g' : G →L[ℝ] E} {s : set G} {x : G} {n : with_top ℕ}
56+
{f g : G → E} {f' g' : G →L[ℝ] E} {s : set G} {x : G} {n : ℕ∞}
5757

5858
include 𝕜
5959

@@ -304,28 +304,28 @@ begin
304304
refl
305305
end
306306

307-
lemma cont_diff_within_at_euclidean {n : with_top ℕ} :
307+
lemma cont_diff_within_at_euclidean {n : ℕ∞} :
308308
cont_diff_within_at 𝕜 n f t y ↔ ∀ i, cont_diff_within_at 𝕜 n (λ x, f x i) t y :=
309309
begin
310310
rw [← (euclidean_space.equiv ι 𝕜).comp_cont_diff_within_at_iff, cont_diff_within_at_pi],
311311
refl
312312
end
313313

314-
lemma cont_diff_at_euclidean {n : with_top ℕ} :
314+
lemma cont_diff_at_euclidean {n : ℕ∞} :
315315
cont_diff_at 𝕜 n f y ↔ ∀ i, cont_diff_at 𝕜 n (λ x, f x i) y :=
316316
begin
317317
rw [← (euclidean_space.equiv ι 𝕜).comp_cont_diff_at_iff, cont_diff_at_pi],
318318
refl
319319
end
320320

321-
lemma cont_diff_on_euclidean {n : with_top ℕ} :
321+
lemma cont_diff_on_euclidean {n : ℕ∞} :
322322
cont_diff_on 𝕜 n f t ↔ ∀ i, cont_diff_on 𝕜 n (λ x, f x i) t :=
323323
begin
324324
rw [← (euclidean_space.equiv ι 𝕜).comp_cont_diff_on_iff, cont_diff_on_pi],
325325
refl
326326
end
327327

328-
lemma cont_diff_euclidean {n : with_top ℕ} :
328+
lemma cont_diff_euclidean {n : ℕ∞} :
329329
cont_diff 𝕜 n f ↔ ∀ i, cont_diff 𝕜 n (λ x, f x i) :=
330330
begin
331331
rw [← (euclidean_space.equiv ι 𝕜).comp_cont_diff_iff, cont_diff_pi],
@@ -338,7 +338,7 @@ section diffeomorph_unit_ball
338338

339339
open metric (hiding mem_nhds_iff)
340340

341-
variables {n : with_top ℕ} {E : Type*} [inner_product_space ℝ E]
341+
variables {n : ℕ∞} {E : Type*} [inner_product_space ℝ E]
342342

343343
lemma cont_diff_homeomorph_unit_ball :
344344
cont_diff ℝ n $ λ (x : E), (homeomorph_unit_ball x : E) :=

0 commit comments

Comments
 (0)