Zulip Chat Archive

Stream: new members

Topic: Typeclasses for Banach Algebra

rtertr (Sonia) (Mar 17 2023 at 19:21):

Hi again,
I have a question regarding going from to this A space. I had to add a few extra conditions on my A.
I am not sure if it still the Banach space. My main issue is now ‖x‖ = ‖↑x‖. Is there anyway this can be true?
And then I was able to before to use iterated_fderiv_eq_equiv_comp and iterated_deriv_eq_iterate.
Can I add some conditions on A such that I am able to use these theorems again?

import data.complex.basic
import analysis.normed_space.exponential
import tactic
import topology.basic
import analysis.calculus.iterated_deriv
import analysis.special_functions.exp_deriv
import number_theory.dioph
import analysis.complex.real_deriv

open complex
open real

noncomputable theory

namespace real

variables {A : Type*} [normed_add_comm_group A] [normed_space  A] [complete_space A] [nontrivially_normed_field A] [normed_space A ] [normed_space A ] [has_lift_t A ]

lemma norm_complex_abs {x:A} {k j:  }:x ^ k * x ^ j = complex.abs x ^ (k + j):=
  rw  pow_add,
  rw complex.norm_eq_abs,

example {x:A}  {n: } {a:}: (λ (x : A),iterated_fderiv  n (λ (x : A), complex.exp (-a * ↑‖x ^ 2))) x = (λ (x : A),deriv^[n] (λ (x : A), complex.exp (-a *  ↑‖x ^ 2)) x) x :=
  rw iterated_fderiv_eq_equiv_comp,
  rw iterated_deriv_eq_iterate,
  simp only [linear_isometry_equiv.norm_map],

end real

Kind regards,

Ruben Van de Velde (Mar 17 2023 at 19:35):

Depends on what coercion that arrow stands for

Kevin Buzzard (Mar 17 2023 at 19:36):

variables {A : Type*} [normed_add_comm_group A] [normed_space ℝ A] [complete_space A] [nontrivially_normed_field A] [normed_space A ℂ] [normed_space A ℝ] [has_lift_t A ℂ]

Are you sure about all that?

Eric Wieser (Mar 17 2023 at 19:41):

Yes, that's definitely not something you want

Kevin Buzzard (Mar 17 2023 at 19:41):

In your code I get an error on norm_cast. The goal is

 x = ‖↑x

If I start clicking on the LHS and unravelling until I find out how this is working (so, more precisely, I click on ‖x‖ then normed_field.to_has_norm then nontrivially_normed_field.to_normed_field), I run into _inst_4: nontrivially_normed_field A. If I click on the RHS and do the same thing (↑x) I rrun into _inst_7: has_lift_t A ℂ. As far as I can see, _inst_4 and _inst_7 are two unrelated constants, so I would guess that ‖x‖ = ‖↑x‖ is not provable and in general not true.

Eric Wieser (Mar 17 2023 at 19:41):

Writing [has_lift_t A B] in a mathematical statement is pretty much always incorrect

Kevin Buzzard (Mar 17 2023 at 19:45):

One issue I have with mathlib is that for parts of the library I'm unfamiliar with, I find it very hard to discover how exactly one is supposed to state random things such as "let AA be a normed R\R-algebra which is a field and such that C\mathbb{C} is a normed space over AA", because you have to have a good feeling about which typeclasses are fundamental, which are mixins, which are data, how you're supposed to be telling the system that various diagrams commute etc. Looking at your code, like Eric I immediately see a code smell with the has_lift_t but there might be other errors too which are harder for me to find. Even in areas I know a bit better I still struggle -- for example even the evening before I was giving a class on unique factorization domains in my course recently, I was desperately asking on the Discord how to say "let AA be a unique factorization domain".

The one thing I do know how to do now though is to debug -- for example discovering that one side depended on _inst_4 and the other side depended on _inst_7 was very easy for me, because of the amazing widgets we have now. So at least I can see that something's wrong quickly rather than bashing my head against the wall trying to solve an unsolvable goal.

Eric Wieser (Mar 17 2023 at 19:46):

but there might be other errors too which are harder for me to find

Indeed, [normed_add_comm_group A] [nontrivially_normed_field A] is also wrong as it defines two different + operators on A

Kevin Buzzard (Mar 17 2023 at 19:47):

Can we lint for this? I'm sure it never happens in mathlib because that code has been reviewed, but it would be great for beginners if stuff like "you just put two norms on A, both called ‖x‖" can be explicitly flagged.

Eric Wieser (Mar 17 2023 at 20:04):

Usually linters are for "you proved this but made a mess". The case you're describing is "you have no hope of proving this because you made a mess so your theorem is false"

Eric Wieser (Mar 17 2023 at 20:18):

You could potentially have a tactic that just tries to find out if multiple different has_add instances can be produced from the context

Eric Wieser (Mar 17 2023 at 20:18):

(and same for all notation_classes)

Jireh Loreaux (Mar 17 2023 at 20:49):

Isn't this literally just the problem of detecting non-defeq diamonds? Because you don't care if you can get the has_add instances two different ways as long as they are the same. And to figure out if there are no non-defeq diamonds you potentially have to traverse all instance paths, right?

I think what seems more feasible to me (and somewhat useful) would be some sort of check where you could could specify some classes to check (e.g., has_add or has_mul) and see if there are disjoint subsets of your context which produce that class.

Although as I write it I realize that disjointness isn't quite the right condition, because you may have something in context which is needed by both things. In particular, if you wanted to know if there were two has_smul R A instances and your context contained [comm_semiring R], [semiring A], [module R A], [algebra R A] then disjoint subsets are no possible. So maybe what we want is distinct minimal collections of hypotheses?

As long as your context isn't huge then this seems somewhat feasible, but it's not something you would want to have running all the time. You would want to call it explicitly, and that seems quite handy, especially for newcomers. I'm imagining an interface like

generate has_smul R A
-- a tactic that shows all the distinct minimal collections of hypotheses in the local context from which you can infer a `has_smul` instance

#generate has_smul R A
-- a command that does the same with whatever currently is included in `#where`.

Jireh Loreaux (Mar 17 2023 at 20:50):

Eric, now that I re-read your message, maybe this is what you meant, but I didn't read it that way the first time.

Jireh Loreaux (Mar 17 2023 at 20:54):

Another thought I had (which I think should be less computationally intensive), would be to consider all structure projections from instances in context and make sure all the data ones with the same name and type are defeq.

Jireh Loreaux (Mar 17 2023 at 20:56):

Note that neither of these is really detecting non-defeq diamonds. The purpose would only be to help you make sure you didn't do something silly.

Eric Wieser (Mar 17 2023 at 21:12):

I'm 90% of the way to a working tactic to do the above

Notification Bot (Mar 17 2023 at 21:12):

17 messages were moved here from #maths > Exponential Banach Algebra by Eric Wieser.

Eric Wieser (Mar 17 2023 at 21:24):


import analysis.normed_space.exponential
import bad

  {A : Type*}
  [normed_add_comm_group A] [normed_space  A] [complete_space A] [nontrivially_normed_field A] [normed_space A ] [normed_space A ] [has_lift_t A ] :
    true :=

Eric Wieser (Mar 17 2023 at 21:25):

This prints a trace message and adds

_inst_4.«bad instances» : has_add A × has_add A :=
  (distrib.to_has_add A (ring.to_distrib A), add_zero_class.to_has_add A (add_monoid.to_add_zero_class A)),
_inst_4.«bad instances» : has_zero A × has_zero A :=
  (mul_zero_class.to_has_zero A (non_unital_non_assoc_semiring.to_mul_zero_class A),
   add_zero_class.to_has_zero A (add_monoid.to_add_zero_class A))

to the context, which you can inspect in the widget view. fst is the instance that come from _inst_4, snd is the instance that comes from omitting _inst_4.

Eric Wieser (Mar 17 2023 at 21:26):

This only works if your assumptions conflict with each other, it doesn't detect conflicts with global instances (so won't tell you that [ring real] is not what you want)

Kevin Buzzard (Mar 17 2023 at 23:11):

What would have solved my problem the other day (and perhaps also Sonia's) would be a thing saying "ok so I've definitely made a UFD now but please tell me which things to delete".

Eric Wieser (Mar 17 2023 at 23:14):

Right, the above doesn't tell you which things to delete

Eric Wieser (Mar 17 2023 at 23:15):

But it does tell you that nontrivially_normed_field A was where things started going wrong

Eric Wieser (Mar 17 2023 at 23:15):

So either you need to remove nontrivially_normed_field A, or work out what was conflicting with it and remove that instead

Kevin Buzzard (Mar 17 2023 at 23:48):

Unfortunately I've seen ring real in the wild :-/

rtertr (Sonia) (Mar 18 2023 at 15:35):

Hello again,
Thank you for all your input! I was trying to adjust my file in to the Banach space, but then it asked for more conditions on A, which I then just added to see how far I could go. It is unfortunate that they are in conflict with each other, but very cool tactic you made, the find_conflict one.
The nontrivially_normed_field A popped up around the time I said
have h₁:=mono_exp_neg_sq_bounded_nonneg_banach n ha, which was of the form
(n : ℕ) {a : ℂ } (ha : 0 < a.re): ∃ (C : ℝ), ∀ x:A, (‖x‖ ≥ 0 → ‖x‖ ^ (n) * complex.abs (complex.exp (-a*↑‖x‖ ^ 2)) ≤ C), which was not proved yet, since I was working backwards.
I think I might just return to (x : fin d → ℝ) for now then, since I am not sure I can you my previous work on the Banach space.
Thank you again :)

Eric Wieser (Mar 18 2023 at 15:51):

To elaborate on the problem; you can't have both [normed_add_comm_group A] [nontrivially_normed_field A] at the same time, just as you can't have [add_comm_group A] [ring A]. But you don't need both, as the latter implies the former. Just use the stronger one, nontrivially_normed_field A

rtertr (Sonia) (Mar 18 2023 at 16:27):

Hmm, I guess I am confused about the nontrivially_normed_field A. Because the condition ∃ (x : α), 1 < ‖x‖ seems fine.
But to show a function is in the Schwartz space, I need to show it is of rapid decrease, which is ∀ (k n : ℕ), ∃ (C : ℝ), ∀ (x : fin d → ℝ), ‖x‖ ^ k * ‖iterated_fderiv ℝ n (λ (x : fin d → ℝ), cexp (-a * ↑‖x‖ ^ 2)) x‖ ≤ C. But is seems all the theorems regarding iterated_fderiv require a nontrivially_normed_field, but I am not sure why fin d → ℝ is not a nontrivially_normed_field.

Kevin Buzzard (Mar 18 2023 at 16:37):

It's not a field. Nonzero elements of fields have inverses. But (0,1) has no inverse.

Eric Wieser (Mar 18 2023 at 16:38):

But is seems all the theorems regarding iterated_fderiv require a nontrivially_normed_field

Can you give an example of such a theorem?

Kevin Buzzard (Mar 18 2023 at 16:39):

I don't know this part of the library well but my guess is that if the system is asking you for a nontrivially normed field then it's presumably expecting you to put in something like the field where the epsilons are living (i.e. probably the reals in your case), rather than the vector spaces where all the functions are going from and to.

rtertr (Sonia) (Mar 18 2023 at 16:42):

So before in my previous proof I was using iterated_deriv_within_eq_equiv_comp.
And then the theorems in https://leanprover-community.github.io/mathlib_docs/analysis/calculus/cont_diff.html#iterated_fderiv seemed to require a nontrivially_normed_field :D

Eric Wieser (Mar 18 2023 at 16:44):

Yes, but you're giving it one when you write iterated_fderiv ℝ. It wants nontrivially_normed_field 𝕜 (𝕜 = ℝ) not nontrivially_normed_field E (E = (fin d → ℝ))

Eric Wieser (Mar 18 2023 at 16:46):

What made you conclude you needed nontrivially_normed_field A? Did you get an error message and add it to fix it?

rtertr (Sonia) (Mar 18 2023 at 16:47):

It was created as a sub-goal :D Let me try to make a #mwe

rtertr (Sonia) (Mar 18 2023 at 16:49):

import data.complex.basic
import analysis.normed_space.exponential
import data.polynomial.basic
import data.polynomial.eval
import tactic
import analysis.special_functions.exp_deriv

open is_absolute_value
open_locale classical big_operators nat complex_conjugate

open polynomial

noncomputable theory

namespace real

variables {A : Type*} [normed_add_comm_group A] [normed_space  A] [complete_space A]

lemma polynomial_mul_exp_neg_sq_bounded_banach (a: )  (ha: 0<a.re):  p : (polynomial ),  (k n : ),  (C : ),  (x:A), x‖^k * (λ (x : A  ), (p.eval ↑‖x) * complex.exp (-a*↑‖x ^ 2)) x  C:= by sorry

lemma deriv_iterative_exp_neg_sq_banach (n : ) (a:):  p : (polynomial  ),  x : A , deriv^[n] (λ (x : A ), complex.exp (-a*↑‖x ^ 2)) x = (λ (x : A  ), (p.eval ↑‖x) * complex.exp (-a*↑‖x ^ 2)) x:= by sorry

lemma gaussian_decay_banach  {d: } {a:}  (ha: 0<a.re):  (k n : ),  (C : ),  (x : A), x ^ k * iterated_fderiv  n (λ (x : A), complex.exp (-a * ↑‖x ^ 2)) x  C :=
  intro k,
  intro n,
  have h₁:=deriv_iterative_exp_neg_sq_banach,
  specialize h₁ n,
  specialize h₁ a,
  obtain p,h₁⟩:=h₁,
  have h₂:= polynomial_mul_exp_neg_sq_bounded_banach a ha,
  specialize h₂ p,
  specialize h₂ k,
  specialize h₂ n,
  obtain C,h₂⟩:=h₂,
  use C,
  intro x,
  rw iterated_fderiv_eq_equiv_comp, -- now allowed to apply
  rw iterated_deriv_eq_iterate,
  simp only [linear_isometry_equiv.norm_map],
  have h₃: (λ (x : A), deriv^[n] (λ (x : A ), complex.exp (-a * ↑‖x ^ 2)) x) x= (λ (x : A),  eval ↑‖x p * complex.exp (-a * ↑‖x ^ 2)) x, by {dsimp, rw h₁ x,},
  have h₄: (λ (x : A), deriv^[n] (λ (x : A ), complex.exp (-a * ↑‖x ^ 2)) x)= (λ (x : A),  eval ↑‖x p * complex.exp (-a * ↑‖x ^ 2)), by {simp only, apply funext h₁,},
  have h₅: (λ (x : A), deriv^[n] (λ (x : A ), complex.exp (-a * ↑‖x ^ 2)) x) x= (λ (x : A  ),  eval ↑‖x p * complex.exp (-a * ↑‖x ^ 2)) x, by exact congr_fun h₄ x,
  simp only at h₃,
  simp only at h₅,
  have h₆: x ^ k * (λ (x : A), deriv^[n] (λ (x : A ), complex.exp (-a * ↑‖x ^ 2)) x) x  C,
    {dsimp only,
    rw h₅,
    exact h₂ x,},
  rw iterated_fderiv_eq_equiv_comp,
  rw iterated_deriv_eq_iterate,
  simp only [linear_isometry_equiv.norm_map],


rtertr (Sonia) (Mar 18 2023 at 16:50):

Not sure it necessarily a subgoal, but when you click at the issue at deriv_iterative_exp_neg_sq_banach, it says

failed to synthesize type class instance for
A : Type u_1,
_inst_1 : normed_add_comm_group A,
_inst_2 : normed_space  A,
_inst_3 : complete_space A,
n : ,
a : ,
p : polynomial ,
x : A
 nontrivially_normed_field A

rtertr (Sonia) (Mar 18 2023 at 16:51):

So I just assumed it was A that needed to be nontrivially_normed_field.

rtertr (Sonia) (Mar 18 2023 at 16:52):

And it is the same if I replace A with fin d → ℝ.

Sebastien Gouezel (Mar 18 2023 at 16:53):

You're confused between docs#iterated_fderiv and docs#iterated_deriv. The former works on any normed space (over some field k), and is a multilinear map. The latter only works on the base field itself, and is a scalar. Just like the right general notion of a derivative is the Frechet derivative, which is a linear map, but when the space you are working on turns out to be the base field then you can canonically identify this linear map with a number.

rtertr (Sonia) (Mar 18 2023 at 17:10):

Okay, great! Thank you for all your help and patience! I will try to work around this then :big_smile:

Last updated: Dec 20 2023 at 11:08 UTC