Typeclasses for Banach Algebra

Stream: new members

[rtertr (Sonia)]

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):=
begin
  rw ← pow_add,
  rw ←complex.norm_eq_abs,
  congr,
  norm_cast,
end

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 :=
begin
  rw iterated_fderiv_eq_equiv_comp,
  rw iterated_deriv_eq_iterate,
  simp only [linear_isometry_equiv.norm_map],
  sorry,
end

end real

Kind regards,
Sonia

[Ruben Van de Velde]

Depends on what coercion that arrow stands for

[Kevin Buzzard]

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]

Yes, that's definitely not something you want

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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 $A$ be a normed $\R$-algebra which is a field and such that $\mathbb{C}$ is a normed space over $A$", 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 $A$ 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]

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]

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]

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]

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]

(and same for all notation_classes)

[Jireh Loreaux]

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]

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]

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]

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]

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

[Notification Bot]

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

[Eric Wieser]

bad.lean

import tactic.core
import data.nat.basic
import algebra.module.basic

-- extended as needed
meta def possible_type_classes : list expr → tactic (list expr)
| [] := pure []
| [x] := do
  list.traverse (λ n, tactic.mk_app n [x])
    [``has_add,
     ``has_zero,
     ``has_mul,
     ``has_one]
| [x, y] := do
  list.traverse (λ n, tactic.mk_app n [x, y])
    [``has_smul]
| _ := pure []

#check tactic.interactive.classical

meta def tactic.interactive.find_conflicts : tactic unit :=
do
  some frozen ← tactic.frozen_local_instances,
  all_bad ← list.join <$> frozen.mmap (λ fi, do
    t ← tactic.infer_type fi,
    args ← list.reverse <$> t.list_explicit_args,
    tactic.trace format!"trying {fi}",
    possible ← possible_type_classes args,
    insts ← list.join <$> possible.mmap (λ p, do
      (some with_fi) ← tactic.try_core (tactic.mk_instance p) | pure [],
      some without_fi ← tactic.retrieve (do
        tactic.unfreeze_local_instances,
        tactic.clear' tt [fi],
        tactic.try_core (tactic.mk_instance p)) | pure [],
      ok ← succeeds (tactic.is_def_eq with_fi without_fi),
      if ok then
        pure []
      else
        pure [(fi, p, with_fi, without_fi)] ),
    pure insts),
  all_bad.mmap (λ i, do
    (fi, p, with_fi, without_fi) ← pure i,
    prod_t ← tactic.mk_app `prod [p, p],
    prod_v ← tactic.mk_app `prod.mk [with_fi, without_fi],
    tactic.definev (fi.local_pp_name ++ `«bad instances») prod_t prod_v),
  match all_bad with
  | [] := tactic.trace "no conflicts"
  | l := tactic.trace format!"Found non-defeq instances, inspect the context for more info"
  end

import analysis.normed_space.exponential
import bad

example
  {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 :=
begin
  find_conflicts,
end

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[rtertr (Sonia)]

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]

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)]

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]

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

[Eric Wieser]

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]

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)]

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]

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]

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

[rtertr (Sonia)]

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

[rtertr (Sonia)]

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

section
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 :=
begin
  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],
end

end

[rtertr (Sonia)]

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)]

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

[rtertr (Sonia)]

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

[Sebastien Gouezel]

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)]

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