asymptotics and the Fréchet derivative #748

avigad · 2019-02-22T00:40:45Z

This is a start on big O and little o calculations and the Fréchet derivative. The header comments in asymptotics and deriv explain what is there.

I am pleased that the proof of the chain rule is reasonably short and readable, a sign that the library is working well.

The next step will be to define the univariate derivative from the Fréchet derivative, so that we can do ordinary calculus, along the lines of #711.

digama0 · 2019-02-22T00:48:12Z

src/analysis/asymptotics.lean

+or.elim (lt_or_ge 0 c)
+  (assume : c > 0, ⟨c, this, hc⟩)
+  (assume h'c : c ≤ 0,
+    have {x : α | ∥f x∥ ≤ 1 * ∥g x∥} ∈ l.sets,


minor suggestion: I think this proof will be shorter if you use max c 1 as the existential witness

I'll take a look, but I don't think that helps.

digama0 · 2019-02-22T00:52:13Z

src/analysis/asymptotics.lean

+
+theorem is_littleo.add {f₁ f₂ : α → β} {g : α → γ} {l : filter α}
+    (h₁ : is_littleo f₁ g l) (h₂ : is_littleo f₂ g l) :
+  is_littleo (f₁ + f₂) g l :=


You used addition of functions here, but used lambda addition for is_bigo.{add,sub} and is_littleo.sub. I'm not sure which is better, but it should be consistent in any case. Probably the lambda addition will avoid some superfluous rewrites?

You are right. Yes, I favored the lambdas, because they work better with rewrites. I'll fix this.

digama0 · 2019-02-22T00:55:32Z

src/analysis/asymptotics.lean

+-/
+
+section
+variables {k : Type*} [normed_field k] [normed_space k β] [has_norm γ]


Can the field be K instead of k? I won't insist on greek but you use k as a number or function in some theorems and as a type in others, and it's a bit disorienting.

kckennylau · 2019-02-22T00:56:57Z

src/analysis/normed_space/bounded_linear_maps.lean

@@ -8,6 +8,7 @@ Continuous linear functions -- functions between normed vector spaces which are
 import algebra.field
 import tactic.norm_num
 import analysis.normed_space.basic
+import ..asymptotics


This might be the first use of .. as file path in mathlib

digama0 · 2019-02-22T00:58:44Z

src/analysis/asymptotics.lean

+"transitivity" rules
+-/
+
+theorem is_bigo_of_is_bigo_of_is_bigo [has_norm β] [normed_group γ] [has_norm δ]


These names look a little unwieldy. How about is_bigo.trans for this and the little o version, and is_littleo.trans_bigo and is_bigo.trans_littleo for the other two? (I admit that they are adhering to the naming convention, though, so maybe an alias is in order, if people actually guess this name.)

kckennylau · 2019-02-22T00:59:18Z

src/analysis/asymptotics.lean

+  is_littleo (f ∘ k) (g ∘ k) (l.comap k) :=
+λ c, mem_comap_sets.mpr ⟨_, hfg c, set.subset.refl _⟩
+
+theorem is_bigo.mono {f : α → β} {g : α → γ} {l₁ l₂ : filter α} (h : l₁ ≤ l₂)


Might @[monotonicity] be used here?

I have never used it. If you are sure it is appropriate, I will add it. Otherwise, I will experiment by adding a local attribute later and see if it works.

kckennylau · 2019-02-22T01:00:31Z

src/analysis/asymptotics.lean

+
+variables [has_norm β] [normed_group γ]
+
+theorem is_bigo_zero {g : α → γ} {l : filter α} :


Maybe one can use is_littleo.to_is_bigo to prove this (by using the theorem below).

digama0 · 2019-02-22T01:00:55Z

src/analysis/asymptotics.lean

+
+theorem is_littleo_of_tendsto [normed_field β] {f g : α → β} {l : filter α}
+    (hgf : ∀ x, g x = 0 → f x = 0) (h : tendsto (λ x, f x / (g x)) l (nhds 0)) :
+  is_littleo f g l :=


This theorem should be merged with the next one

kckennylau · 2019-02-22T01:01:31Z

src/analysis/asymptotics.lean

+@[simp]
+theorem is_bigo_norm_left {f : α → β} {g : α → γ} {l : filter α} :
+  is_bigo (λ x, ∥f x∥) g l ↔ is_bigo f g l :=
+by simp only [is_bigo, norm_norm]


Thanks for using simp only here 😝

kckennylau · 2019-02-22T01:03:26Z

src/analysis/asymptotics.lean

+  intros c cpos,
+  filter_upwards [h₁ (2 * c), h₂ (2 * c)],
+  intros x hx₁ hx₂, dsimp at hx₁ hx₂,
+  have : 0 < (2 : real), by norm_num,


kckennylau · 2019-02-22T01:04:41Z

src/analysis/asymptotics.lean

+theorem is_bigo_mul_left {f : α → β} {g : α → γ} {l : filter α} {c : β} (hc : c ≠ 0) :
+  is_bigo (λ x, c * f x) g l ↔ is_bigo f g l :=
+begin
+  have cne0 : ∥c∥ ≠ 0, by rw [ne, norm_eq_zero]; exact hc,


mt norm_eq_zero.1 hc?

digama0 · 2019-02-22T01:06:46Z

src/analysis/normed_space/bounded_linear_maps.lean

@@ -44,6 +45,9 @@ lemma is_linear_map.with_bound

 namespace is_bounded_linear_map

+def to_linear_map {f : E → F} (h : is_bounded_linear_map f) : E →ₗ[k] F :=


f should be explicit here, because h gets omitted in term printouts, so it's really confusing looking at to_linear_map _

kckennylau · 2019-02-22T01:09:45Z

src/analysis/asymptotics.lean

+    ⟨c', hc'⟩     := h₂ in
+begin
+  use c * c',
+  filter_upwards [hc, hc'], dsimp,


Is the dsimp necessary here?

@kckennylau It is (and everywhere else I use it). filter_upwards leaves hypotheses x ∈ { x | ... } and rewrite doesn't do well with these. Is there a better way to contract these?

digama0 · 2019-02-22T01:10:27Z

src/analysis/normed_space/deriv.lean

+  tendsto (λ x', ∥x' - x∥⁻¹ • (f x' - f x - f' (x' - x))) (nhds_within x s) (nhds 0)
+
+def has_fderiv_at (f : E → F) (f' : E → F) (x : E) :=
+has_fderiv_at_within f f' x set.univ


This is the definition I was talking about yesterday. You should define

has_deriv_at f f' x := is_bounded_linear_map f' ∧ tendsto (λ x', ∥x' - x∥⁻¹ • (f x' - f x - f' (x' - x))) (nhds x) (nhds 0)

and then prove this equality.

This seems like a really bad idea. The point is that all the theorems about fderiv expressed in terms of has_deriv_at_within will work right out of the box for has_deriv_at. If we do it your way, we either need two versions of every theorem or we will have to do a rewrite every time we want to apply one. Am I missing something?

In fact, I think we ought to unify continuous_at_within and continuous_at in this way. I have already chafed with the mistmatch.

digama0 · 2019-02-22T01:13:51Z

src/analysis/normed_space/deriv.lean

+
+def has_fderiv_at_within (f : E → F) (f' : E → F) (x : E) (s : set E) :=
+is_bounded_linear_map f' ∧
+  tendsto (λ x', ∥x' - x∥⁻¹ • (f x' - f x - f' (x' - x))) (nhds_within x s) (nhds 0)


Why aren't you using the is_littleo version as the definition? It should unfold better than this one

Why do you think the is_littleo version is better? tendsto is central to our library and the tendsto version was convenient for most of the theorems in the file. My guess is that this is the more convenient definition.

kckennylau · 2019-02-22T01:14:42Z

src/analysis/normed_space/deriv.lean

+theorem has_fderiv_neg {f : E → F} {f' : E → F} {x : E} {s : set E}
+    (h : has_fderiv_at_within f f' x s) :
+  has_fderiv_at_within (λ x, - f x) (λ x, - f' x) x s :=
+(has_fderiv_smul (-1 : ℝ) h).congr (by simp) (by simp)


The type ascription (-1 : ℝ) is not necessary because has_fderiv_smul only accepts real number as first argument.

Removing it results in an error. I think the elaborator tries to elaborate the negation before it infers the type.

digama0 · 2019-02-22T01:15:19Z

src/analysis/normed_space/deriv.lean

+  end
+
+def has_fderiv_at_within_mono {f : E → F} {f' : E → F} {x : E} {s t : set E}
+    (h : has_fderiv_at_within f f' x t) (hst : s ⊆ t) :


These two arguments should be swapped, and it should be has_fderiv_at_within.mono and not a def

digama0 · 2019-02-22T01:15:58Z

src/analysis/normed_space/deriv.lean

+theorem has_fderiv_at_within.congr {f₀ f₁ : E → F} {f₀' f₁' : E → F}
+    {x : E} {s : set E} (h : has_fderiv_at_within f₀ f₀' x s)
+    (h₀ : ∀ x, f₀ x = f₁ x) (h₁ : ∀ x, f₀' x = f₁' x) :
+  has_fderiv_at_within f₁ f₁' x s :=


This theorem should end with an iff

kckennylau · 2019-02-22T01:16:26Z

src/analysis/normed_space/deriv.lean

+  has_fderiv_at_within (λ x, f x - g x) (λ x, f' x - g' x) x s :=
+has_fderiv_add hf (has_fderiv_neg hg)
+
+theorem continuous_of_has_fderiv {f : E → F} {f' : E → F} {x : E} {s : set E}


Might this proof be shortened by using o-analysis? This seems like a reasonable second touchstone for the o-analysis library other than the chain rule below.

I'll give it a try.

Done. Soon I'll update the PR with a nicer version.

digama0 · 2019-02-22T01:18:18Z

src/analysis/normed_space/deriv.lean

+  has_fderiv_at_within f₁ f₁' x s :=
+by rw [←(funext h₀ : f₀ = f₁), ←(funext h₁ : f₀' = f₁')]; exact h
+
+theorem has_fderiv_id (x : E) (s : set E) : has_fderiv_at_within id id x s :=


These theorems should first be proven as just has_fderiv_at id id x, and then there is a general theorem that has_fderiv_at implies has_deriv_at_within.

It seems that the intended general theorem has s substituted for set.univ...

That's true, but we need both versions of the theorems in any case.

This is my point. We don't need two versions or a translation if has_fderiv_at is defined the right way.

digama0 · 2019-02-22T01:21:43Z

src/order/filter/basic.lean

@@ -1104,6 +1107,12 @@ lemma tendsto_cong {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
  (h : tendsto f₁ l₁ l₂) (hl : {x | f₁ x = f₂ x} ∈ l₁.sets) : tendsto f₂ l₁ l₂ :=
 by rwa [tendsto, ←map_cong hl]

+theorem tendsto.congr {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β}
+    (h : tendsto f₁ l₁ l₂) (h' : ∀ x, f₁ x = f₂ x) :
+  tendsto f₂ l₁ l₂ :=


this should be an iff

Actually, is this necessary at all? This is just congr; ext

So the proofs that use this theorem should use convert instead?

Oh, I see now how this can come up in a proof. I guess this version also has its uses, although the arguments should be flipped (it will still work with projection notation). But I think this can be one line proved by by rw <- funext h'; exact h or by convert h; ext; apply h'

Yes, I have found that this functions as a proof-term version of convert (which I have come to really enjoy).

digama0 · 2019-02-22T01:23:32Z

src/topology/basic.lean

@@ -549,6 +549,21 @@ have h₁ : ∃ (i : set α), i ∈ {t : set α | a ∈ t ∧ is_open t},
  from ⟨set.univ, set.mem_univ _, is_open_univ⟩,
 by { rw [nhds_within_eq, map_binfi_eq h₀ h₁], simp only [map_principal] }

+theorem tendsto_nhds_within_mono_left {f : α → β} {a : α}
+    {s t : set α} {l : filter β} (h : tendsto f (nhds_within a t) l) (hst : s ⊆ t) :


The two final arguments should be flipped here and in the next theorem

src/analysis/normed_space/deriv.lean

avigad · 2019-02-23T15:54:08Z

This version addresses all the comments in the reviews. I made all the changes, except for @kckennylau's suggestion to use the [monotonicity] attribute. I'll try it at some point and add it if it works.

In addition, I improved definitions and proofs in asymptotics, added more useful properties, and wrote a nicer proof of the fact that differentiability implies continuity. The commits have been rebased and tested with the current master.

sgouezel · 2019-02-23T21:28:55Z

src/analysis/normed_space/deriv.lean

+import topology.basic analysis.normed_space.bounded_linear_maps ..asymptotics tactic.abel
+open filter asymptotics
+
+variables {E : Type*} [normed_space ℝ E]


Is there really something specific in this file to real numbers, or would everything go through for the complex numbers or the p-adics, say?

I just tried changing the variable declarations to this:

variables {K : Type*} [normed_field K] variables {E : Type} [normed_space K E] variables {F : Type} [normed_space K F] variables {G : Type} [normed_space K G] include K

I don't see why it shouldn't work, since ultimately norms are put on everything. But the declaration causes the elaborator to fail miserably everywhere. Tracing class instances doesn't make it clear what is going wrong. One guess is that the problem has to do with the fact that a normed_field is also an instance of a normed_space (I think).

I move to accept the PR as is, so that anyone who wants to get the generalization to work can give it a try.

I think it fails because normed_space etc are no longer out_param, so you have to make K explicit everywhere.

avigad · 2019-03-01T03:37:13Z

Changes:

renamed is_bigo to is_O, is_littleo to is_o
adopted Mario's changes and additions, but added an expanded proof of the chain rule as an example
generalized to normed spaces over any normed field to cover e.g. the complex numbers and the p-adics.

…and additions

…ed field

digama0 reviewed Feb 22, 2019

View reviewed changes

kckennylau reviewed Feb 22, 2019

View reviewed changes

digama0 reviewed Feb 22, 2019

View reviewed changes

kckennylau reviewed Feb 22, 2019

View reviewed changes

digama0 reviewed Feb 22, 2019

View reviewed changes

kckennylau reviewed Feb 22, 2019

View reviewed changes

digama0 reviewed Feb 22, 2019

View reviewed changes

kckennylau reviewed Feb 22, 2019

View reviewed changes

digama0 reviewed Feb 22, 2019

View reviewed changes

kckennylau reviewed Feb 22, 2019

View reviewed changes

digama0 reviewed Feb 22, 2019

View reviewed changes

kckennylau reviewed Feb 22, 2019

View reviewed changes

digama0 reviewed Feb 22, 2019

View reviewed changes

jdsalchow reviewed Feb 22, 2019

View reviewed changes

src/analysis/normed_space/deriv.lean Outdated Show resolved Hide resolved

cipher1024 assigned digama0 Feb 22, 2019

sgouezel reviewed Feb 23, 2019

View reviewed changes

avigad added 3 commits March 1, 2019 10:05

feat(*): add various small lemmas

91c55d4

feat(analysis/asymptotics): start on bigo and littlo

876d392

feat(analysis/normed_space/deriv): start on derivative

e5cb19a

avigad and others added 8 commits March 1, 2019 10:05

feat(analysis/asymptotics,analysis/normed_space/deriv): improvements …

e8c62d1

…and additions

fix(asymptotics, deriv): minor formatting fixes

ea963a9

add has_fderiv_at_filter

36b4213

fix(*): fix things from change tendsto_congr -> tendsto.congr'

b76e147

feat(analysis/*): is_bigo -> is_O, is_littleo -> is_o

ee4e460

feat(analysis/normed_space/deriv): add readable proof of chain rule

28ce4b6

feat(analysis/normed_space/deriv): generalize to spaces over any norm…

fa6a3bf

…ed field

refactor(analysis/asymptotics): minor formatting changes

da39986

avigad merged commit 04b5f88 into leanprover-community:master Mar 1, 2019


		variables [has_norm β] [normed_group γ]

		theorem is_bigo_zero {g : α → γ} {l : filter α} :

		@@ -44,6 +45,9 @@ lemma is_linear_map.with_bound

		namespace is_bounded_linear_map

		def to_linear_map {f : E → F} (h : is_bounded_linear_map f) : E →ₗ[k] F :=

asymptotics and the Fréchet derivative #748

asymptotics and the Fréchet derivative #748

Conversation

avigad commented Feb 22, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Feb 22, 2019 • edited Loading

Choose a reason for hiding this comment

kckennylau Feb 22, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

avigad commented Feb 23, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

avigad commented Mar 1, 2019

digama0 Feb 22, 2019 •

edited

Loading

kckennylau Feb 22, 2019 •

edited

Loading