division of DualNumbers

Stream: Is there code for X?

[Frederick Pu]

Is there any code or division of DualNumbers? More specifically Div (DualNumber F) where F is a field. If not, would it be possible for me to get a pull request from formalizing it? Right now I working on some proofs about negative binomials that geometric sequences on DualNumbers would really help with.

[Yaël Dillies]

If @Eric Wieser doesn't have it then nobody has it

[Eric Wieser]

You can work with Units (DualNumber _) to get division of invertible elements. If you also want support for non-invertible elements; what do you intend to define 1/eps as?

[Frederick Pu]

Frederick Pu said:

Is there any code or division of DualNumbers? More specifically Div (DualNumber F) where F is a field. If not, would it be possible for me to get a pull request from formalizing it? Right now I working on some proofs about negative binomials that geometric sequences on DualNumbers would really help with.

Here's a quick demo of what I've done so far with division:

Definition of division:

noncomputable instance : Div (DualNumber ℝ) :=
{
  div := fun ⟨a, b⟩ ⟨c, d⟩ => ⟨a/c, (b*c - a*d)/c^2⟩
}

Basic lemmas to make proofs easier

theorem div_eq (a b : DualNumber ℝ) : a / b = ⟨a.fst / b.fst, (a.snd * b.fst - a.fst * b.snd) / b.fst^2⟩ := by rfl
theorem add_eq (a b : DualNumber ℝ) : a + b = ⟨a.fst + b.fst, a.snd + b.snd⟩ := by exact rfl
theorem diff_eq (a b : DualNumber ℝ) : a - b = ⟨a.fst - b.fst, a.snd - b.snd⟩ := by exact rfl

Basic arithmetic equations:

theorem sum_one_div (a b : DualNumber ℝ) (ha : a.fst ≠ 0) (hb : b.fst ≠ 0) : 1 / a + 1 / b = (b + a) / (a*b) := by
  ...
theorem diff_one_div (a b : DualNumber ℝ) (ha : a.fst ≠ 0) (hb : b.fst ≠ 0) : 1 / a - 1 / b = (b - a) / (a*b) := by
  ...

Projection equations:

theorem fst_one_div_real (a : ℝ) : (1 / TrivSqZeroExt.inl a : DualNumber ℝ).1 = 1 / a := by
  rw [div_eq]
  simp
theorem snd_one_div_real (a : ℝ) : (1 / TrivSqZeroExt.inl a : DualNumber ℝ).2 = 0 := by
  rw [div_eq]
  simp

Putting it all together into a usage example:

example (a b : ℝ) (ha : a ≠ 0) : ε / (TrivSqZeroExt.inl a + (TrivSqZeroExt.inl b)*DualNumber.eps : DualNumber ℝ) = ε * (1 / (TrivSqZeroExt.inl a)) := by
  rw [div_eq]
  apply congr_arg₂

  simp
  apply Or.inl
  rfl

  simp [fst_one_div_real, snd_one_div_real]
  field_simp
  have : (ε :DualNumber ℝ).2 = 1 := by rfl
  rw [this]
  ring

[Eric Wieser]

Something to watch out for here; you should not use .1(Prod.fst) on dual numbers; you should use .fst (TrivSqZeroExt.fst) instead

[Eric Wieser]

Similarly, using ⟨re, dual⟩ will get you into trouble because this is Prod.mk; the API assumes you will write algebraMap _ _ re + dual*eps instead (or inl re + inr dual)

[Frederick Pu]

Eric Wieser said:

You can work with Units (DualNumber _) to get division of invertible elements. If you also want support for non-invertible elements; what do you intend to define 1/eps as?

I'm thinking of treating division as the deriv operator. That is if the division exists than it is well defined but otherwise it'll give a garbage output of $0 + 0\epsilon$.

[Frederick Pu]

Eric Wieser said:

Something to watch out for here; you should not use .1(Prod.fst) on dual numbers; you should use .fst (TrivSqZeroExt.fst) instead

Please correct me if I'm wrong but it feels like using the Prod notation makes a lot of elementary proofs easier to do using simp.

For example:

theorem fst_one_div_real (a : ℝ) : (1 / TrivSqZeroExt.inl a : DualNumber ℝ).1 = 1 / a := by
  rw [div_eq]
  simp
theorem snd_one_div_real (a : ℝ) : (1 / TrivSqZeroExt.inl a : DualNumber ℝ).2 = 0 := by
  rw [div_eq]
  simp

[Kevin Buzzard]

If you're only looking to divide by units then I would define Inv to be inverse on units and 0 off them, I would consider using IsUnit rather than a.1 != 0 as your normal form, and I would define Div to be a * b^{-1}.

[Eric Wieser]

Please correct me if I'm wrong but it feels like using the Prod notation makes a lot of elementary proofs easier to do using simp.

The rest of the TrivSqZeroExt API is not written with Prod.fst and Prod.snd, so if you use these functions then Mathlib has nothing to offer you

[Eric Wieser]

I think those lemmas are a bad example, because you should just prove them with rfl anyway

[Eric Wieser]

Anyway, I think this is close enough to iterate on; could you make a PR adding Div for TrivSqZeroExt?

[Frederick Pu]

Eric Wieser said:

I think those lemmas are a bad example, because you should just prove them with rfl anyway

Yeah I would love to. I don't think I have access to any of the mathlib sub-branches though

[Kim Morrison]

What do you mean by sub-branches?

[Kevin Buzzard]

I conjecture that Frederick might mean that they would like push access to non-master branches? What's your GitHub userid Frederick? It's not in your profile.

Or tell us what you actually meant :-)

[Frederick Pu]

Yeah that's what I meant. In the the "how to contribute to mathlib" page it said that you should get accesss to a non-master branch. Also, should I develop a lot of the lemma for it first or just start by commiting the definition?

[Kevin Buzzard]

Well you can't do any of those things until you answer the question about your GitHub userid. I think a reasonable PR would be the definition of Inv and Div, and some basic lemmas. As a general rule I wouldn't go over 100 lines for the first PR.

[Eric Wieser]

You need to tell us your github username (or put it in your zulip profile) for us to give you access :)

[Frederick Pu]

Ok my user id for github is FrederickPu

[Eric Wieser]

Invite sent!

[Eric Wieser]

Regarding the generalization to TrivSqZeroExt; I think it's something like

instance : Inv (tsze R M) where
  inv x := ⟨x.fst⁻¹, -(x.fst⁻¹ •> x.snd <• x.fst⁻¹)⟩

[Frederick Pu]

Created the pull request. I just did it using HDiv instead of inverses since I feel like it would be weird to assume that the internal division of M and R sepereatly should have anything to do with how they interact with eachother. Although this may lead to some compatibility issue in the future since I was mainly thinking about TrivExtZero R R

[Eric Wieser]

The case to be careful of is TrivSqZeroExt R R when R is non-commutativie

[Eric Wieser]

In the non-commutative case, division is a pretty useless operator, since it only lets you write a * inv b not inv a * b. So I think it is better to approach this thinking about defining the inverse; and then define division such that a / b = a * inv b, perhaps with a slightly nicer implementation.

The important thing is to prove a div_eq_mul_inv lemma!

[Frederick Pu]

Oh sorry should I redo it and submit another PR or wait till you reject my current one first?

[Eric Wieser]

You can edit the PR in place, no need to redo it or delete it; just make another commit with the changes and push again

[Eric Wieser]

Ah sorry, you do need to redo this

[Eric Wieser]

Because you pushed to origin, not upstream

[Frederick Pu]

Also it seems like the definition of inv should be more like this:

instance inv [HSub R M M] [Mul R] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] : Inv (tsze R M) :=
  ⟨fun b => (b.1⁻¹, (b.1 - b.2) <• (b.1 * b.1)⁻¹)⟩

[Frederick Pu]

But HSub R M M is a bit sketch

[Frederick Pu]

ok. Can I get some feed back of my definition before I submit a PR?

[Eric Wieser]

The best place for feedback is in the PR itself!

[Eric Wieser]

Frederick Pu said:

Also it seems like the definition of inv should be more like this:

instance inv [HSub R M M] [Mul R] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] : Inv (tsze R M) :=
  ⟨fun b => (b.1⁻¹, (b.1 - b.2) <• (b.1 * b.1)⁻¹)⟩

But I can tell you that your hunch is right, HSub R M M is too sketchy for this to be reasonable

[Eric Wieser]

I think you made an error when substituting $$1 + 0\eps$$, and that b.1 should be 0.

[Frederick Pu]

Which of these do you think is better?

instance inv [HSub R M M] [Mul R] [Field R] [Semiring M] [SMul Rᵐᵒᵖ M] [SMul R M] : Inv (tsze R M) :=
  ⟨fun b => (b.1⁻¹, (b.1 * (b.1 * b.1)⁻¹)  •> (1:M) + (b.2 <• (b.1 * b.1)⁻¹))⟩

instance inv [HSub R M M] [Mul R] [Inv R] [One M] [Add M] [SMul Rᵐᵒᵖ M] [SMul R M] : Inv (tsze R M) :=
  ⟨fun b => (b.1⁻¹, (b.1 * (b.1 * b.1)⁻¹)  •> (1:M) + (b.2 <• (b.1 * b.1)⁻¹))⟩

[Frederick Pu]

I feel like the Field and Semiring conditions nicely encapsulate the requirements but might be too restrictive if someone wants to go crazy

[Eric Wieser]

Eric Wieser said:

Regarding the generalization to TrivSqZeroExt; I think it's something like

instance : Inv (tsze R M) where
  inv x := ⟨x.fst⁻¹, -(x.fst⁻¹ •> x.snd <• x.fst⁻¹)⟩

I'm pretty sure this one is right, as it matches docs#fderiv_inv'

[Eric Wieser]

1 : M is suspicious in your code above too; remember that (1 : tsze R M) = inl (1 : R) + inr (0 : M)

[Eric Wieser]

So if you take your division formula for fun ⟨a, b⟩ ⟨c, d⟩ => ⟨a/c, (b*c - a*d)/c^2⟩, you should be subsituting a = 1 and b = 0.

[Eric Wieser]

Frederick Pu said:

I feel like the Field and Semiring conditions nicely encapsulate the requirements but might be too restrictive if someone wants to go crazy

I am afraid that a lot of the design of TrivSqZeroExt is precise because someone wanted to go crazy with non-commutative rings (such as the dual quaternions); that someone is me.

[Frederick Pu]

Eric Wieser said:

Eric Wieser said:

Regarding the generalization to TrivSqZeroExt; I think it's something like

instance : Inv (tsze R M) where
  inv x := ⟨x.fst⁻¹, -(x.fst⁻¹ •> x.snd <• x.fst⁻¹)⟩

I'm pretty sure this one is right, as it matches docs#fderiv_inv'

Wait so M is responsible for the negativeness? also why not group the inverses together?

[Eric Wieser]

Because grouping together inverses in the derivative of x⁻¹ is a lie told to you by commutative algebraists :devil:

[Eric Wieser]

Wait so M is responsible for the negativeness?

I don't think it really matters; in any real situation docs#neg_smul and docs#smul_neg applies anyway

[Frederick Pu]

@[simps apply]
def inlHom [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] : R →+* tsze R M where

It seems like R usually carries more ring structure

[Eric Wieser]

In that example, neither R nor M have negation

[Frederick Pu]

so might as well put the negative in :shrug:

[Eric Wieser]

The version with negation is [Ring R] [AddCommGroup M], in which case both have negation

[Frederick Pu]

Oh sorry

[Eric Wieser]

Here's an argument for why it should be M and not R; if you assume some kind of derivative model, then maybe R is the space of positive reals; the derivative of a function that's always positive can sometimes be negative, so arguably it's the differential piece (M) that should be carrying the negation

[Frederick Pu]

theorem snd_list_prod [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M]
    [SMulCommClass R Rᵐᵒᵖ M] (l : List (tsze R M))

[Frederick Pu]

Eric Wieser said:

Here's an argument for why it should be M and not R; if you assume some kind of derivative model, then maybe R is the space of positive reals; the derivative of a function that's always positive can sometimes be negative, so arguably it's the differential piece (M) that should be carrying the negation

that's a good point, but why is always somethign R over M?

[Eric Wieser]

What do you mean by "over"?

[Frederick Pu]

Never mind, I thought that semirings had inverses for some reason

[Eric Wieser]

It's an easy mistake to make, mathlib is full of generalizations you don't usually have to think about

[Frederick Pu]

The interface is actually pretty clean i think:

instance inv [Neg M] [Inv R] [SMul Rᵐᵒᵖ M] [SMul R M] : Inv (tsze R M) :=
  ⟨fun b => (b.1⁻¹,  - (b.1⁻¹ •> b.2 <• b.1⁻¹))⟩

[Frederick Pu]

Also how do you motivate using b.1⁻¹ •> b.2 <• b.1⁻¹ vs b.2 <• b.1⁻¹ <• b.1⁻¹

[Eric Wieser]

Now you should define Div as well, and prove that the two agree

[Eric Wieser]

The motivation will appear when you try to prove that x * x⁻¹ = 1 for [DivisionRing R] and x.fst \ne 0

[Frederick Pu]

but if you're doing DivisionRing don't you have commutivity?

[Eric Wieser]

Nope, a division ring is a field without commutativity!

[Frederick Pu]

ahhhhh

[Eric Wieser]

(I think in French the words are swapped in some way, though I might be misremembering)

[Frederick Pu]

I'm not french tho, just a dumb undergrad

[Eric Wieser]

If you're writing lean code as an undergrad you're probably not dumb :)

[Eric Wieser]

Perhaps it's worth considering a more fun way to play this game:

• Define division and inverses in a way that works on fields and vector spaces, prove they work well with multiplication
• Once you have that working, try to remove commutativity

[Frederick Pu]

here's what I got so far:

theorem mul_inv [DivisionRing R] [AddCommGroup M] [Module Rᵐᵒᵖ M] [Module R M] {x : tsze R M} (hx : fst x ≠ 0) :
  x * x⁻¹ = 1 := by
{
  ext
  rw [fst_mul, fst_inv, fst_one, mul_inv_cancel hx]
  rw [snd_mul, snd_inv, smul_neg, ← smul_assoc, smul_eq_mul, mul_inv_cancel hx, one_smul, fst_inv, add_left_neg, snd_one]
}

[Frederick Pu]

it's tough because you need the module to bring the negative to the outside

[Frederick Pu]

actually no you don't I don't know what was requiring me to have a Module

[Eric Wieser]

I think it's fine to assume a module if you need it

[Frederick Pu]

But module requires addcommgroup

[Eric Wieser]

One again, no it doesn't; at least, not in mathlib!

[Frederick Pu]

Screenshot-2024-04-11-174407.png

[Frederick Pu]

So you still need commutivity on M no?

[Eric Wieser]

This is referring to additive commutativity, a + b = b + a

[Frederick Pu]

so you dont care about addcommgroup?

[Eric Wieser]

Only really crazy people care about non-commutative addition

[Frederick Pu]

the thing is don't really need addcommgroup in the proof. You're never swapping terms

[Eric Wieser]

Frederick Pu said:

so you dont care about addcommgroup?

What you've written looks good to me

[Frederick Pu]

is there a semimodule or smth

[Eric Wieser]

Yes, but in mathlib it's written Module

[Eric Wieser]

A semimodule is just a module without negation, but we established you need negation on M anyway

[Frederick Pu]

how can they have the exact same name?

[Frederick Pu]

oh cause no mul comm i see what u mean

[Frederick Pu]

Ok, submitting the PR

[Frederick Pu]

How do I run the linter on my local machine

[Eric Wieser]

Can you write the PR number here after a # so that it auto-Links?

[Eric Wieser]

The style linter can be run with scripts/lint-style.sh

[Eric Wieser]

The other linter can be run by writing #lint in the file (and deleting it when you're done)

[Notification Bot]

95 messages were moved from this topic to #new members > making pull requests by Eric Wieser.

[Frederick Pu]

Do you know where I can find proofs of the following lemmas?

have op_smul_smul : ((fst x)⁻¹ •> (snd x <• (fst x)⁻¹)) <• fst x  = (fst x)⁻¹ •> ((snd x <• (fst x)⁻¹) <• fst x) := by sorry
have op_smul_assoc : (snd x <• (fst x)⁻¹ <• fst x) = (snd x <• ((fst x)⁻¹ <• fst x)) := by sorry
have op_smul_one : (snd x) <• (1:R) = snd x := by sorry

[Eric Wieser]

The first one needs [SMulCommClass R Rᵐᵒᵖ M], then is smul_comm

[Eric Wieser]

simp? or rw? can maybe help find the others

[Frederick Pu]

I got the first and the third one but the second one is giving me grief

[Frederick Pu]

Actually I don't think this second equation holds

[Kevin Buzzard]

Can you make a #mwe if you want other people to think about your question?

[Frederick Pu]

Kevin Buzzard said:

Can you make a #mwe if you want other people to think about your question?

I should have used op_smul_op_smul instead

[Frederick Pu]

How long do you think until I will be able to use this on dual numbers?

theorem tsum_geometric_of_norm_lt_one{K : Type u_4} [NormedField K] {ξ : K} (h : ‖ξ‖ < 1) :
∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹

[Eric Wieser]

You won't be able to use that theorem as written, because dual numbers don't form a field or even a division ring (eps has no invers)

[Frederick Pu]

so will we need to reprove the theorem but for whatever the dual numbers are?

[Frederick Pu]

Maybe NormedRing, and it holds for all units

[Frederick Pu]

I feel like if you know convergence then u don't really use any field properties to prove the geometric series, just dividing by the common ratio, which is ok if it's not eps

[Eric Wieser]

I think a good goal would be to prove that lemma for just DualNumbers, then work out the generalizatoin when you have the proof

[Frederick Pu]

Yeah, but I'm gonna need the fact that the geometric sequence is summable in the first place. Which is some metric space stuff

[Eric Wieser]

We _do_ have a metric space on the dual numbers

[Frederick Pu]

should be fine then

[Frederick Pu]

Do u think I need anymore api stuff on TrivEqZeroExt inorder to get started?

[Eric Wieser]

I think it would be great to polish the PR on Inv and DIv first; then embark on that larger goal

[Frederick Pu]

Ok, should I edit my actual pull request comment?

[Frederick Pu]

also did you see my latest pull request, I proved all the lemmas u asked (except for 1/eps because I can't find that in Triv)

[Eric Wieser]

No, I didn't! looking at #12075 now

[Frederick Pu]

theorem summable_iff_vanishing_norm{ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E} :
Summable f ↔ ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → ‖Finset.sum t fun (i : ι) => f i‖ < ε

just so i remember

[Eric Wieser]

Frederick Pu said:

also did you see my latest pull request, I proved all the lemmas u asked (except for 1/eps because I can't find that in Triv)

That would go in the DualNumber.lean file; it's fine to edit multiple files in the same PR if the changes are closely related.

[Antoine Chambert-Loir]

Frederick Pu said:

how can they have the exact same name?

In Mathlib, the docs#Module structure just adds the scalar action of R on M and how it interacts with addition. The interaction with negation, if there is some negation on M by way of a docs#AddCommGroup structure on M, the interaction of scalar multiplication with neg or subtraction comes for free.

[Frederick Pu]

Can anyone explain why tsum_mul_left isn't solvling this goal?

import Mathlib.Algebra.DualNumber
import Mathlib.Topology.Algebra.InfiniteSum.Ring

example {R : Type*} [DivisionRing R] (p : DualNumber R) [TopologicalSpace (DualNumber R)] [T2Space (DualNumber R)] (f : Nat → DualNumber R):
  ∑' (i : Nat), p^i = 1 + p * ∑' (x : Nat), f x := by
{
  have : ∑' (x : Nat), p * f x = p * ∑' (x : Nat), f x := tsum_mul_left
}
#check tsum_mul_left

[Frederick Pu]

Frederick Pu said:

Can anyone explain why tsum_mul_left isn't solvling this goal?

import Mathlib.Algebra.DualNumber
import Mathlib.Topology.Algebra.InfiniteSum.Ring

example {R : Type*} [DivisionRing R] (p : DualNumber R) [TopologicalSpace (DualNumber R)] [T2Space (DualNumber R)] (f : Nat → DualNumber R):
  ∑' (i : Nat), p^i = 1 + p * ∑' (x : Nat), f x := by
{
  have : ∑' (x : Nat), p * f x = p * ∑' (x : Nat), f x := tsum_mul_left
}
#check tsum_mul_left

Oh my bad, DualNumbers arent a DivisionRing. Seem like we need to basically redo a lot of the tsum lemmas

[Frederick Pu]

Actually Summable.tsum_mul_left seems fine

[Eric Wieser]

Note hat instead of assuming TopologicalSpace (DualNumber R) you should import the TrivSqZeroExt file in analysis

[Eric Wieser]

@loogle NormedSpace, TrivSqZeroExt

[loogle]

:search: TrivSqZeroExt.instL1NormedSpace, TrivSqZeroExt.instL1NormedAlgebra

[Kevin Buzzard]

Eric Wieser said:

Note hat instead of assuming TopologicalSpace (DualNumber R) you should import the TrivSqZeroExt file in analysis

Just to be clear here -- Eric is saying that writing [TopologicalSpace (DualNumber R)] is mathematically wrong, because it means "put a completely arbitrary topology on the dual numbers which is completely unrelated to the algebraic structure".

[Eric Wieser]

I guess you can fix "completely unrelated"by adding [TopologicalRing (DualNumber R)], but that's still probably "related but not in the ways you would expect"

[Frederick Pu]

yeah I noticed that the typeclasses required for tsum_left_mul and summable_of_vanishing_norm seem to really not like eachother for some reason

[Eric Wieser]

Can you show what you wrote?

[Eric Wieser]

This sounds a bit like "Semiring and AddCommGroup don't like each other", for which the answer is "of course not, that has two different +s; use Ring instead"

[Frederick Pu]

Screenshot-2024-04-14-164702.png
Screenshot-2024-04-14-164719.png

[Eric Wieser]

Please paste code (as a #mwe) not images!

[Frederick Pu]

theorem bruh.{u_3, u_1} {ι : Type u_1} {R : Type u_3} [SeminormedAddCommGroup (DualNumber R)]
  [CompleteSpace (DualNumber R)] {f : ι → (DualNumber R)} (x : DualNumber R): Summable (fun i : Nat => x) := by
{
/--
ι : Type u_1
R : Type u_3
inst✝¹ : SeminormedAddCommGroup (DualNumber R)
inst✝ : CompleteSpace (DualNumber R)
f : ι → DualNumber R
x : DualNumber R
⊢ ∀ ε > 0, ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖Finset.sum t fun i ↦ x‖ < ε
--/
  rw [summable_iff_vanishing_norm]
}

works but

theorem bruh.{u_3, u_1} {ι : Type u_1} {R : Type u_3} [SeminormedAddCommGroup (DualNumber R)]

  [CompleteSpace (DualNumber R)] [Ring (DualNumber R)] {f : ι → (DualNumber R)} (x : DualNumber R): Summable (fun i : Nat => x) := by

{
/ --
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  Summable ?m.9232
--/
  rw [summable_iff_vanishing_norm]

}

doesn't

[Frederick Pu]

so adding [Ring (DualNumber R)] breaks the type inference

[Ruben Van de Velde]

Please read #mwe

[Ruben Van de Velde]

And you should never have a [Ring (Concrete type)] argument

[Frederick Pu]

okay, let's go back to this example then:

import Mathlib.Algebra.DualNumber
import Mathlib.Topology.Algebra.InfiniteSum.Ring
import Mathlib.Analysis.Normed.Group.InfiniteSum

theorem extracted_1.{u_1} {R : Type u_1} [inst : DivisionRing R] [inst_1 : TopologicalSpace (DualNumber R)]
    [inst_2 : TopologicalSemiring (DualNumber R)] (p : DualNumber R) (h : Summable fun i ↦ p ^ i)
    [inst_3 : T2Space (DualNumber R)] : ∑' (i : ℕ), p ^ i = 1 + p * ∑' (x : ℕ), p ^ x := sorry

[Frederick Pu]

I think we need to be able to infer TopologicalSpace (DualNumber R) from TopologicalSpace R

[Frederick Pu]

Shouldn't this be from the product topology?

[Eric Wieser]

Like I said above, you're missing an import

[Kevin Buzzard]

I have a mathematical question. You seem to want to put a topology on the dual numbers. What topology do you want to put on it?

[Eric Wieser]

You also seem to want a norm (from an earlier message); what norm do you want?

[Frederick Pu]

The topology for R^2, since we want to treat it like a normed vector space

[Eric Wieser]

@loogle TrivSqZeroExt, TopologicalSpace

[loogle]

:search: TrivSqZeroExt.instTopologicalSpace, TrivSqZeroExt.continuous_fst, and 44 more

[Eric Wieser]

That is the topology that matches R²; but you have to import that file for Lean to find it automatically

[Frederick Pu]

TrivSqZeroExt.instL1NormedAddCommGroup

[Frederick Pu]

I think that's pretty good, also matches the signature of our inverse lemmas

[Kevin Buzzard]

So I asked you which topology, and you replied "I have a specific topology in mind", and that's why stuff like [inst_1 : TopologicalSpace (DualNumber R)] must be wrong, because there you're saying "put an arbitrary topology on it" (you can see it must be wrong becuase there is no mention of the topology you want). And I don't understand your answer -- R is just a random division ring. What is "the topology for R^2"?

[Frederick Pu]

Those instances were just to test the lemmas I was using. I think I'm gonna have R be topological ring and then take the the product topology

[Kevin Buzzard]

I guess I am a bit confused about what you're trying to achieve at this point.

[Frederick Pu]

That the theorem for geometric series applies for DualNumbers. that is:
1 + p + p^2 + p^3 +.... = 1/(1 - p) for $p.snd \neq 0$

[Kevin Buzzard]

That's not true -- for example it's not true if p=1+eps or if p=37+eps.

[Frederick Pu]

I think you need the additional condition of ||p|| < 1

[Frederick Pu]

Basically I'm trying have the geo_normed_field thing work for rings with units

[Jireh Loreaux]

IIRC @Eric Wieser had some ideas about generalizing this to certain topological rings, but maybe I'm misremembering and it was about exp instead.

[Eric Wieser]

What's a "geo_normed_field"?

[Eric Wieser]

@Frederick Pu , are you looking for docs#NormedRing.tsum_geometric_of_norm_lt_one ?

[Eric Wieser]

Ah no, that's not the statement I expected

[Frederick Pu]

theorem tsum_geometric_of_norm_lt_one{K : Type u_4} [NormedField K] {ξ : K} (h : ‖ξ‖ < 1) :
∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹

[Frederick Pu]

theorem geom_series_mul_neg {R : Type u_4} [NormedRing R] [CompleteSpace R] (x : R) (h : ‖x‖ < 1) :
(∑' (i : ℕ), x ^ i) * (1 - x) = 1

[Frederick Pu]

the second one should be easy to use for dualnumbers

[Eric Wieser]

I made #12164 which generalizes the first lemma to DivisionRing, but indeed that doesn't help you here

[Frederick Pu]

Here's the minimum you need for it to work:

import Mathlib.Algebra.DualNumber
import Mathlib.Analysis.NormedSpace.TrivSqZeroExt
import Mathlib.Analysis.SpecificLimits.Normed

example {R : Type*} [NormedRing R] [CompleteSpace R] (x : DualNumber R) (h : ‖x‖ < 1) :
  (∑' (i : ℕ), x ^ i) * (1 - x) = 1 :=
  geom_series_mul_neg x h

[Frederick Pu]

i think u get NormedRing (DualNumber R) and CompleteSpace (DualNumber R) for free because of products or smth

[Eric Wieser]

Mathlib indeed has both of those instances already

[Eric Wieser]

(You get it for free because I contributed it to mathlib as a very small part of my PhD!)

[Frederick Pu]

theorem geom_series_of_fst_ne_zero {R : Type*} [NormedDivisionRing R] [CompleteSpace R] (x : DualNumber R) (h : ‖x‖ < 1) (h1 : x.fst ≠ 1) :
    (∑' (i : ℕ), x ^ i) = (1 - x : DualNumber R)⁻¹ := by
  have := geom_series_mul_neg x h
  have w : ((∑' (i : ℕ), x ^ i) * (1 - x)) * (1 - x)⁻¹ = (1 - x)⁻¹ := by
    rw [this, one_mul]
  rw [← w, mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]

  rw [TrivSqZeroExt.fst_sub]
  exact sub_ne_zero_of_ne h1.symm

[Eric Wieser]

Are you sure you need ‖x‖ < 1? Is ‖x.fst‖ < 1 enough?

[Frederick Pu]

isnt ||a + bε|| = sqrt(a^2 + b^2)

[Eric Wieser]

The one in mathlib is ‖a + bε‖ = ‖a‖ + ‖b‖

[Frederick Pu]

then how is ||x.fst|| < 1 enough?

[Frederick Pu]

intuitively i don't think you can just ignore the derivative component

[Eric Wieser]

The derivative component is n*x.fst^(n-1)* x.snd (at least, in the commutative case), which should converge irrespective of the value of x.snd

[Frederick Pu]

yee that makes sense

[Eric Wieser]

Frederick Pu said:

theorem geom_series_mul_neg {R : Type u_4} [NormedRing R] [CompleteSpace R] (x : R) (h : ‖x‖ < 1) :
(∑' (i : ℕ), x ^ i) * (1 - x) = 1

So this won't actually help for that stronger result; but it would be great to prove it anyway

[Frederick Pu]

Eric Wieser said:

Frederick Pu said:

theorem geom_series_mul_neg {R : Type u_4} [NormedRing R] [CompleteSpace R] (x : R) (h : ‖x‖ < 1) :
(∑' (i : ℕ), x ^ i) * (1 - x) = 1

So this won't actually help for that stronger result; but it would be great to prove it anyway

wdym. That's already in mahthlib

[Eric Wieser]

Oh! Usually people write docs#geom_series_mul_neg (which creates an automatic link) to talk about things that already exist

[Frederick Pu]

sorry I didn't know

[Eric Wieser]

No worries, good job on finding it

[Frederick Pu]

I think this lemma is missing from DualNumber.lean:

example {R : Type*} [Ring R] (x : DualNumber R) (n : Nat) :
    x^n = inl (x.fst ^ n) + inr (n * x.fst ^ (n - 1) * x.snd) := by
  sorry

[Frederick Pu]

is it in TrivSqZeroExt?

[Eric Wieser]

I think generally the API tries to avoid writing lemmas like that right now

[Eric Wieser]

Instead it has docs#TrivSqZeroExt.fst_pow and docs#TrivSqZeroExt.snd_pow

[Eric Wieser]

The expectation is that if you're going to split it into components, you want to handle them separately rather than double the number of terms in the expression

[Frederick Pu]

so is there tsum x = inl (tsum.fst) + inr (tsum.snd)

[Eric Wieser]

No, but there is docs#TrivSqZeroExt.fst_tsum

[Eric Wieser]

... or not

[Eric Wieser]

I guess I only added docs#TrivSqZeroExt.hasSum_fst

[Frederick Pu]

also on a side note, can loogle search based on doc comments? seems like that would make it a lot easier to find stuff

[Eric Wieser]

Frederick Pu said:

so is there tsum x = inl (tsum.fst) + inr (tsum.snd)

This is false, because if only the fst part converges the LHS is 0 and the rhs is inl (tsum _)

[Eric Wieser]

Eric Wieser said:

No, but there is docs#TrivSqZeroExt.fst_tsum

This would be false for the same reason

[Frederick Pu]

the thing is those go in the wrong direction. We need to show if fst and snd converge than the sequence converges

[Eric Wieser]

The secret is that you rarely want to show "the sequence converges"; "the sequence converges to x" is much more interesting, and this is what docs#HasSum means

[Eric Wieser]

I think you want (TrivSqZeroExt.hasSum_inl _).add (TrivSqZeroExt.hasSum_inr _)

[Eric Wieser]

I guess it's probably reasonable to add something like HasSum (fun x => (f x).fst) a.fst -> HasSum (fun x => (f x).snd) a.snd -> HasSum f a

[Eric Wieser]

Which should follow fairly immediately from my .add message above.

[Eric Wieser]

It's probably even true as an Iff

[Eric Wieser]

There's a lot missing here because I developed just as much as I needed for docs#TrivSqZeroExt.fst_exp (and the rest of that file) and little else.

[Frederick Pu]

what about something like this:

theorem hasSum_inl_inr (f g : Nat → ℝ) (a b : ℝ) : HasSum f a → HasSum g b → (HasSum (fun n => (inl (f n) + inr (g n) : (DualNumber ℝ))) (inl a + inr b : DualNumber ℝ)) := by
{
  intro hf hg
  apply HasSum.add
  apply TrivSqZeroExt.hasSum_inl
  exact hf
  apply TrivSqZeroExt.hasSum_inr
  exact hg
}

[Eric Wieser]

For this type of thing it's often more useful to have the free variable in the conclusion

[Frederick Pu]

lean seems to get really confused when u tryy to use hasSum_inl directly

[Eric Wieser]

(TrivSqZeroExt.hasSum_inl _ hf).add (TrivSqZeroExt.hasSum_inr _ hg) should work for that?

[Frederick Pu]

it doesnt

[Eric Wieser]

Edited: see if you can see how I worked out the fix from the error message

[Frederick Pu]

oh the extra _

[Frederick Pu]

but why tho, the lemma only takes 1 input

[Notification Bot]

This topic was moved here from #general > Is there any code or division of DualNumbers? by Eric Wieser.

[Eric Wieser]

Frederick Pu said:

but why tho, the lemma only takes 1 input

What makes you say that?

[Frederick Pu]

theorem hasSum_inr [AddCommMonoid R] [AddCommMonoid M] {f : α → M} {a : M} (h : HasSum f a)

[Frederick Pu]

only 1 non implicit argument right?

[Eric Wieser]

Nope, there's a variable line higher up that adds more

[Eric Wieser]

You can read off the variables by hovering over hasSum_inr and reading the tooltip instead of the source

[Frederick Pu]

I feel like in this case it's better to prove that the sequence converges and then get the value this converges to afterward. Since evaluating the sum of i * x^{i - 1} is very nasty

[Kevin Buzzard]

It's just the derivative of the sum of x^i which is 1/(1-x)

[Frederick Pu]

Yeah but the whole point of using dual numbers was to bypass using derivatives

[Kevin Buzzard]

Another approach is just to multiply by (1-x)^2 and observe that a miracle occurs

[Frederick Pu]

But wouldn't that trick still require you to assume convergence in the first place?

[Frederick Pu]

The only trick like that I know is from kumon where you multiply by x, and when u subtract the two sequences you get a geoemtric sequence or smth

[Frederick Pu]

anyhow I'm stuck with this chonker for now that I'll have to golf later

example (x : DualNumber ℝ) (x : DualNumber ℝ) (hx1 : |x.fst| < 1) (hx2 : x.fst ≠ 0):
  Summable (fun i : Nat => x^i) := by
{
  have : (fun i : Nat => x^i) = (fun i : Nat => (inl (x.fst ^ i) + inr ((i:ℝ) * x.fst ^ (i.pred) * x.snd))) := by
    ext i
    · rw [fst_pow, fst_add, fst_inl, fst_inr, add_zero]

    · rw [snd_pow, snd_add, snd_inl, snd_inr, zero_add, ← smul_assoc, smul_eq_mul, nsmul_eq_mul]
  rw [this]
  apply Summable.add
  suffices h :  Summable (fun b => x.fst ^ b) by {
    match h with
    | ⟨t, ht⟩ => {
      use (inl t)
      exact TrivSqZeroExt.hasSum_inl _ ht
    }
  }
  rw [summable_geometric_iff_norm_lt_one]
  exact hx1

  suffices h :  Summable (fun b : Nat => (b:ℝ) * fst x ^ Nat.pred b * snd x) by {
    match h with
    | ⟨t, ht⟩ => {
      use (inr t)
      exact TrivSqZeroExt.hasSum_inr _ ht
    }
  }
  apply Summable.mul_right
  -- apply summable_of_ratio_test_tendsto_lt_one _
  -- sorry
  have : Filter.Tendsto (fun n ↦ ‖↑(n + 1) * fst x ^ Nat.pred (n + 1)‖ / ‖↑n * fst x ^ Nat.pred n‖) Filter.atTop (nhds ‖x.fst‖) := by {
    have : Filter.EventuallyEq (Filter.atTop) (fun n:Nat ↦ ‖(n + 1 : ℝ) / n‖ * ‖x.fst‖) (fun n => ‖↑(n + 1) * fst x ^ Nat.pred (n + 1)‖ / ‖↑n * x.fst ^ (n.pred)‖) := by {
      rw [Filter.EventuallyEq, Filter.eventually_atTop]
      use 1
      intro b hb
      cases h : b with
      | zero => {
        linarith
      }
      | succ b => {
        simp
        have : |(b + 1 : ℝ)| * |fst x| ^ b ≠ 0 := by {
          apply mul_ne_zero
          rw [h] at hb
          simp only [ne_eq, abs_eq_zero]
          intro _
          linarith

          rw [ne_eq, pow_eq_zero_iff', abs_eq_zero]
          tauto
        }
        field_simp
        ring
      }
    }
    rw [Filter.tendsto_congr' this.symm]
    {
      have : Filter.Tendsto (fun n:Nat ↦ ‖((n + 1 : Nat) : ℝ) / ↑n‖) Filter.atTop (nhds (1:ℝ)) := by {
        have : (fun n:Nat ↦ ‖((n + 1 : Nat) : ℝ) / ↑n‖) =ᶠ[Filter.atTop] (fun n:Nat ↦ 1 + (n:ℝ)⁻¹) := by {
          rw [Filter.EventuallyEq, Filter.eventually_atTop]
          use 1
          intro b hb
          have : b ≠ 0 := by linarith
          rw [Real.norm_eq_abs, abs_of_pos]
          field_simp
          apply div_pos
          push_cast
          linarith
          have : (1:Nat) ≤ (b : ℝ) := by
            rw [Nat.cast_le]
            exact hb
          push_cast at this
          linarith
        }
        rw [Filter.tendsto_congr' this]

        have crux1 : Filter.Tendsto (fun n : Nat ↦ (1 : ℝ)) Filter.atTop (nhds 1) :=
          tendsto_const_nhds
        have crux2 : Filter.Tendsto (fun n : Nat ↦ (n:ℝ)⁻¹) Filter.atTop (nhds 0) :=
          tendsto_inverse_atTop_nhds_zero_nat
        have := Filter.Tendsto.add crux1 crux2
        rw [add_zero] at this
        exact this
      }
      have := Filter.Tendsto.mul_const (‖fst x‖) this
      push_cast at this
      rw [one_mul] at this
      exact this
    }
  }

  exact summable_of_ratio_test_tendsto_lt_one hx1 (by {
    rw [Filter.eventually_atTop]
    use 1
    intro b hb
    cases b with
    | zero => simp at hb
    | succ b => {
      simp
      intro h
      cases h with
      | inl l => linarith
      | inr r => exact hx2 r.left
    }
  }) this

}

[Frederick Pu]

Here's the golfed version:

theorem wow (x : DualNumber ℝ) (hx : x.fst ≠ 0) :
      Filter.Tendsto (fun n ↦ ‖↑(n + 1) * fst x ^ Nat.pred (n + 1)‖ / ‖↑n * fst x ^ Nat.pred n‖) Filter.atTop (nhds ‖x.fst‖) := by
  have : Filter.EventuallyEq (Filter.atTop) (fun n:Nat ↦ ‖(n + 1 : ℝ) / n‖ * ‖x.fst‖) (fun n => ‖↑(n + 1) * fst x ^ Nat.pred (n + 1)‖ / ‖↑n * x.fst ^ (n.pred)‖) := by
    rw [Filter.EventuallyEq, Filter.eventually_atTop]
    use 1
    intro b hb
    cases h : b with
    | zero => linarith
    | succ b =>
      simp
      have : |(b + 1 : ℝ)| * |fst x| ^ b ≠ 0 := by
        apply mul_ne_zero
        rw [h] at hb; simp only [ne_eq, abs_eq_zero]; linarith
        rw [ne_eq, pow_eq_zero_iff', abs_eq_zero]; tauto
      field_simp
      ring
  rw [Filter.tendsto_congr' this.symm]
  have : Filter.Tendsto (fun n:Nat ↦ ‖((n + 1 : Nat) : ℝ) / ↑n‖) Filter.atTop (nhds (1:ℝ)) := by
    have : (fun n:Nat ↦ ‖((n + 1 : Nat) : ℝ) / ↑n‖) =ᶠ[Filter.atTop] (fun n:Nat ↦ 1 + (n:ℝ)⁻¹) := by
      rw [Filter.EventuallyEq, Filter.eventually_atTop]
      use 1
      intro b hb
      rw [Real.norm_eq_abs, abs_of_pos]
      field_simp [show b ≠ 0 by linarith]
      exact div_pos (by push_cast; linarith) (by linarith [show (b : ℝ) ≥ 1 by exact Nat.one_le_cast.mpr hb])
    rw [Filter.tendsto_congr' this]

    have crux1 : Filter.Tendsto (fun n : Nat ↦ (1 : ℝ)) Filter.atTop (nhds 1) :=
      tendsto_const_nhds
    have crux2 : Filter.Tendsto (fun n : Nat ↦ (n:ℝ)⁻¹) Filter.atTop (nhds 0) :=
      tendsto_inverse_atTop_nhds_zero_nat
    have := Filter.Tendsto.add crux1 crux2
    rw [add_zero] at this
    exact this
  have := Filter.Tendsto.mul_const (‖fst x‖) this
  push_cast at this
  rw [one_mul] at this
  exact this

example (x : DualNumber ℝ) (hx1 : |x.fst| < 1) (hx2 : x.fst ≠ 0):
      Summable (fun i : Nat => x^i) := by
  have : (fun i : Nat => x^i) = (fun i : Nat => (inl (x.fst ^ i) + inr ((i:ℝ) * x.fst ^ (i.pred) * x.snd))) := by
    ext i
    · rw [fst_pow, fst_add, fst_inl, fst_inr, add_zero]
    · rw [snd_pow, snd_add, snd_inl, snd_inr, zero_add, ← smul_assoc, smul_eq_mul, nsmul_eq_mul]
  rw [this]
  apply Summable.add
  suffices h :  Summable (fun b => x.fst ^ b) by
    match h with
    | ⟨t, ht⟩ =>
      use (inl t)
      exact TrivSqZeroExt.hasSum_inl _ ht
  rw [summable_geometric_iff_norm_lt_one]
  exact hx1

  suffices h :  Summable (fun b : Nat => (b:ℝ) * fst x ^ Nat.pred b * snd x) by
    match h with
    | ⟨t, ht⟩ =>
      use (inr t)
      exact TrivSqZeroExt.hasSum_inr _ ht

  exact Summable.mul_right x.snd <|
   summable_of_ratio_test_tendsto_lt_one hx1 (by {
    rw [Filter.eventually_atTop]
    use 1
    intro b hb
    cases b with
    | zero => simp at hb
    | succ b => {
      simp
      intro h
      cases h with
      | inl l => linarith
      | inr r => exact hx2 r.left
    }
  }) (wow x hx2)

wow just prooves that u can atlually use ratio test

[Frederick Pu]

also smth like this should take us home

example  {R : Type*} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : R) :
  Summable (fun i ↦ x ^ i) → (∑' (i : ℕ), x ^ i) * (1 - x) = 1 := by {
    intro this
    have := this.hasSum.mul_right (1 - x)
    refine' tendsto_nhds_unique this.tendsto_sum_nat _
    have : Filter.Tendsto (fun n : ℕ ↦ 1 - x ^ n) Filter.atTop (nhds 1) := by
      simpa using tendsto_const_nhds.sub (show Filter.Tendsto (fun n ↦ x ^ n) Filter.atTop (nhds 0) by sorry)
    convert← this
    rw [← geom_sum_mul_neg, Finset.sum_mul]
  }

[Eric Wieser]

I think that last one is true much more generally, it doesn't need a norm at all

[Frederick Pu]

Can you have tsum without norm

[Eric Wieser]

Yes, T2Space and TopologicalAddGroup is enough

[Frederick Pu]

theorem womp  {R : Type*} [TopologicalSpace R] [Ring R] [inst : TopologicalRing R] [T2Space R] (x : R) :
  Summable (fun i ↦ x ^ i) → Filter.Tendsto (fun n ↦ x ^ n) Filter.atTop (nhds 0) →  (∑' (i : ℕ), x ^ i) * (1 - x) = 1 := by {
    intro h1 h2
    have := h1.hasSum.mul_right (1 - x)
    refine' tendsto_nhds_unique this.tendsto_sum_nat _
    have : Filter.Tendsto (fun n : ℕ ↦ 1 - x ^ n) Filter.atTop (nhds 1) := by
      simpa using tendsto_const_nhds.sub h2
    convert← this
    rw [← geom_sum_mul_neg, Finset.sum_mul]
  }

[Frederick Pu]

here's a rough sketch of the final proof:

example (x : DualNumber ℝ) (hx1 : |x.fst| < 1) (hx2 : x.fst ≠ 0):
  (∑' (i : ℕ), x ^ i) * (1 - x) = 1 := by {
    apply womp
    exact summable_geom_dual_real x hx1 hx2
    have : (fun i : Nat => x^i) = (fun i : Nat => (inl (x.fst ^ i) + inr ((i:ℝ) * x.fst ^ (i.pred) * x.snd))) := by
      ext i
      · rw [fst_pow, fst_add, fst_inl, fst_inr, add_zero]
      · rw [snd_pow, snd_add, snd_inl, snd_inr, zero_add, ← smul_assoc, smul_eq_mul, nsmul_eq_mul]
    rw [this]
    rw [show (0:DualNumber ℝ) = inl 0 + inr 0 by simp]
    apply Filter.Tendsto.add
    {
      apply Filter.Tendsto.comp (continuous_inl.tendsto 0)
      exact tendsto_pow_atTop_nhds_zero_of_norm_lt_one hx1
    }
    {
      apply Filter.Tendsto.comp (continuous_inr.tendsto 0)
      rw [show 0 = 0 * x.snd by sorry]
      apply Filter.Tendsto.mul_const
      suffices Filter.Tendsto (fun k:Nat ↦ ↑k * fst x ^ k) Filter.atTop (nhds 0) by sorry
      exact tendsto_self_mul_const_pow_of_abs_lt_one hx1
    }

  }

[Eric Wieser]

Here's womp with even fewer assumptions:

theorem Summable.hasSum_geom_sries_mul_sub
    {R : Type*} [TopologicalSpace R] [Ring R] [TopologicalRing R]
    (x : R) (hx : Summable (x ^ ·)) :
    HasSum (fun i => x ^ i * (1 - x)) 1 := by
  obtain ⟨a, hx⟩ := hx
  have hx' := hx
  rw [← hasSum_nat_add_iff' 1, Finset.sum_range_one, pow_zero] at hx'
  simp_rw [mul_sub, mul_one, ←pow_succ]
  simpa using hx.sub hx'

[Eric Wieser]

(you can use HasSum.tsum_eq to get the tsum version)

[Frederick Pu]

theorem Summable.hasSum_geom_sries_mul_sub

    {R : Type*} [TopologicalSpace R] [Ring R] [TopologicalRing R]

    (x : R) (hx : Summable (x ^ ·)) :

    HasSum (fun i => x ^ i * (1 - x)) 1 := by

  obtain ⟨a, hx⟩ := hx

  have hx' := hx

  rw [← hasSum_nat_add_iff' 1, Finset.sum_range_one, pow_zero] at hx'

  simp_rw [mul_sub, mul_one, ←pow_succ]

  simpa using hx.sub hx'

theorem womp  {R : Type*} [TopologicalSpace R] [Ring R] [inst : TopologicalRing R] [T2Space R] (x : R) :

  Summable (fun i ↦ x ^ i)  →  (∑' (i : ℕ), x ^ i) * (1 - x) = 1 := by {

    intro h1

    have := h1.hasSum.mul_right (1 - x)

    have :   ∑' (i : ℕ), (x ^ i * (1 - x))  = (∑' (i : ℕ), x ^ i) * (1 - x) := by sorry -- tsum_mul_right

    rw [← this]

    exact HasSum.tsum_eq <| Summable.hasSum_geom_sries_mul_sub x h1

  }

example (x : DualNumber ℝ) (hx1 : |x.fst| < 1) (hx2 : x.fst ≠ 0):

      (∑' (i : ℕ), x ^ i) * (1 - x) = 1 :=

  womp x <| summable_geom_dual_real x hx1 hx2

[Mitchell Lee]

You can show the summability by using docs#hasSum_coe_mul_geometric_of_norm_lt_one

[Eric Wieser]

We started with that but the side z-condition is too strong I think?

[Kevin Buzzard]

Right, nilpotent things should have norm infinitesimally small (ie however big the value of r is, r * epsilon should have norm less than 1)

[Eric Wieser]

That's not possible with our signature for norms, right? The closest we could do is set the norm to zero, but then we don't have a t2 space and our sums don't converge to a single value

[Kevin Buzzard]

Yes that's right, this is a higher rank valuation, not a rank one (aka real-valued) valuation (aka norm).

[Kevin Buzzard]

I don't even know if it works in the Archimedean case to be honest! In my examples the underlying norm on the base ring R is nonarchimedean and then the extension to infinitesimals is untroublesome

[Mitchell Lee]

Eric Wieser said:

We started with that but the side z-condition is too strong I think?

What does that mean?

I am just pointing out that it seems Frederick was using the ratio test to prove the convergence of a certain series of real numbers, when the convergence of that series (and its value) is already in mathlib.

[Mitchell Lee]

Kevin Buzzard said:

Yes that's right, this is a higher rank valuation, not a rank one (aka real-valued) valuation (aka norm).

If you put a topology on $\mathbb{R}[\epsilon]/\epsilon^2$ using this higher rank norm, wouldn't that make $\mathbb{R}\epsilon$ open? Then it would be difficult for anything to converge.

[Antoine Chambert-Loir]

Kevin Buzzard said:

Right, nilpotent things should have norm infinitesimally small (ie however big the value of r is, r * epsilon should have norm less than 1)

Why should they? Nilpotent operators usually don't have a zero operator norm.

[Kevin Buzzard]

They do for the supremum seminorm on an affinoid

[Kevin Buzzard]

But actually I'm confused about this for two reasons -- first that the reals aren't nonarchimedean and secondly that valuations are supposed to be multiplicative

[Frederick Pu]

The dual numbers have L_p norm, so both the real and derivative components are equally important. The thing is that (a + b\e) ^n = a^n + a^(n-1)b\e. So you can consider the sums seperately.

[Mitchell Lee]

Kevin Buzzard said:

But actually I'm confused about this for two reasons -- first that the reals aren't nonarchimedean and secondly that valuations are supposed to be multiplicative

It seems that in mathlib, the norm of a normed ring is only required to be submultiplicative. (docs#NormedRing) The definition of a normed field requires the norm to be (exactly) multiplicative, though. (docs#NormedField)

It wouldn't be possible to put an (exactly) multiplicative norm on the dual numbers, because they are not a domain.

[Mitchell Lee]

Also, it is possible I am misunderstanding something, but I don't think it is desirable for $\|\epsilon\|$ to be infinitesimal. If it were, then the sequence $1, \frac{1}{2}, \frac{1}{3}, \ldots$ wouldn't converge, because it never comes within $\|\epsilon\|$ of $0$. So the inclusion $\mathbb{R} \to \mathbb{R}[\epsilon]/\epsilon^2$ would not be continuous. This is a problem even if $\mathbb{R}$ is replaced by a nonarchimedean ring.

I think the coefficientwise product topology on $\mathbb{R}[\epsilon]/\epsilon^2$ is the "correct" one.

[Antoine Chambert-Loir]

If $\mathbf R[\varepsilon]/(\varepsilon^2)$ is endowed with the $\ell^1$-norm, one gets a normed algebra structure ($(x+y\varepsilon)(x'+y'\varepsilon)=xx'+(xy'+x'y)\varepsilon$ has norm $|xx'|+|xy'+x'y| \leq (|x|+|y|)(|x'|+|y'|)$), and the geometric series $\sum (x+y\varepsilon)^n$ is summable provided the (necessary) condition $|x|<1$ holds.

[Eric Wieser]

That normed algebra structure is in mathlib

[Frederick Pu]

yeah... how does lean know which norm to inherit?

[Eric Wieser]

Lean just finds the only norm that mathlib provides, which for dual numbers is the L1 norm