[Merged by Bors] - feat: add `HasSum f a → HasProd (exp ∘ f) (exp a)` #12635

MichaelStollBayreuth · 2024-05-03T18:01:32Z

This adds lemmas saying that HasSum f a implies HasProd (exp ∘ f) (exp a) for exp = rexp, cexp, NormedSpace.exp.

While the rexp and cexp versions could be deduced from the NormedSpace.exp one, we give a direct proof (and so avoid needing to import stuff about NormedSpace.exp for these results; the proofs are also a bit faster that way).

Based on the discussion below, this also renames Filter.Tendsto.exp to Filter.Tendsto.rexp for the version specific to the real exponential function, so that Filter.Tendsto.exp can be used for the corresponding statement involving NormedSpace.exp.

See here on Zulip.

sgouezel · 2024-05-04T12:35:20Z

Mathlib/Analysis/NormedSpace/Exponential.lean

@@ -473,6 +473,12 @@ theorem exp_continuous : Continuous (exp 𝕂 : 𝔸 → 𝔸) := by
  exact continuousOn_exp
 #align exp_continuous NormedSpace.exp_continuous

+open Topology in
+lemma _root_.Filter.Tendsto.NormedSpace_exp {α : Type*} {l : Filter α} {f : α → 𝔸} {a : 𝔸}


I don't think NormedSpace_exp is compatible with the naming convention. exp_normedSpace looks better, although not great.

The naming convention is not really explicit on how to deal with names containing a namespace like NormedSpace.exp when they show up as part of lemma names. Unfortunately, Filter.Tendsto.exp is already claimed by the real exponential function.
Would NormedSpace.Filter.Tendsto.exp be a reasonable alternative?

You really want to be able to use dot notation, so it has to be Filter.Tendsto.something. The something could be normedSpaceExp or exp_normedSpace or exp_of_normedSpace. Maybe the best option is indeed normedSpaceExp because it's a single atom, and we need a way to separate it from the other ones. Or just exp, and use rexp and cexp for the real and complex version (I think that's my favorite option).

I'm renaming Filter.Tendsto.exp to Filter.Tendsto.rexp and then Filter.Tendsto.NormedSpace_exp to Filter.Tendsto.exp.

sgouezel · 2024-05-04T12:35:51Z

Mathlib/Analysis/SpecialFunctions/Exponential.lean

+variable {𝕂 𝔸 : Type*} [RCLike 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
+
+/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
+lemma HasSum.NormedSpace_exp {ι : Type*} {f : ι → 𝔸} {a : 𝔸} (h : HasSum f a) :


NormedSpace.hasSum_exp perhaps? Although this would make dot notation on HasSum unavailable here.

You really want dot notation. As above, I'd go for HasSum.exp, and use rexp and cexp for the real and complex versions.

Using HasSum.exp now (I'm already using .rexp for the real exponential version).

Did you forget to push this change?

Looks like I actually forgot to change it... Thanks for spotting it!

Ruben-VandeVelde · 2024-05-04T20:17:03Z

Mathlib/Analysis/SpecialFunctions/Exp.lean

    Tendsto (fun x => exp (f x)) l (𝓝 (exp z)) :=
  (continuous_exp.tendsto _).comp hf
-#align filter.tendsto.exp Filter.Tendsto.exp
+#align filter.tendsto.exp Filter.Tendsto.rexp

 variable [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α}

 nonrec
 theorem ContinuousWithinAt.exp (h : ContinuousWithinAt f s x) :


I think we want to do the same to these, but I wouldn't object if you wanted to do that in a follow-up

That's perhaps mission creep for this PR. But I agree that it should be done, and I can have a look.

Ruben-VandeVelde · 2024-05-04T20:18:28Z

Mathlib/Analysis/SpecialFunctions/Exponential.lean

+variable {𝕂 𝔸 : Type*} [RCLike 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
+
+/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
+lemma HasSum.NormedSpace_exp {ι : Type*} {f : ι → 𝔸} {a : 𝔸} (h : HasSum f a) :


Did you forget to push this change?

Mathlib/Analysis/SpecialFunctions/Exp.lean

Ruben-VandeVelde

maintainer merge

github-actions · 2024-05-05T08:16:56Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

sgouezel · 2024-05-05T09:55:44Z

bors r+

This adds lemmas saying that ` HasSum f a` implies `HasProd (exp ∘ f) (exp a)` for `exp = rexp, cexp, NormedSpace.exp`. While the `rexp` and `cexp` versions could be deduced from the `NormedSpace.exp` one, we give a direct proof (and so avoid needing to import stuff about `NormedSpace.exp` for these results; the proofs are also a bit faster that way). Based on the discussion below, this also renames `Filter.Tendsto.exp` to `Filter.Tendsto.rexp` for the version specific to the real exponential function, so that `Filter.Tendsto.exp` can be used for the corresponding statement involving `NormedSpace.exp`. See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exp.28tsum.29.20.3D.20tprod.28exp.29/near/436891747) on Zulip. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

mathlib-bors · 2024-05-05T11:23:32Z

Build failed (retrying...):

Build

This adds lemmas saying that ` HasSum f a` implies `HasProd (exp ∘ f) (exp a)` for `exp = rexp, cexp, NormedSpace.exp`. While the `rexp` and `cexp` versions could be deduced from the `NormedSpace.exp` one, we give a direct proof (and so avoid needing to import stuff about `NormedSpace.exp` for these results; the proofs are also a bit faster that way). Based on the discussion below, this also renames `Filter.Tendsto.exp` to `Filter.Tendsto.rexp` for the version specific to the real exponential function, so that `Filter.Tendsto.exp` can be used for the corresponding statement involving `NormedSpace.exp`. See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exp.28tsum.29.20.3D.20tprod.28exp.29/near/436891747) on Zulip. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

mathlib-bors · 2024-05-05T11:45:04Z

Build failed (retrying...):

Build

This adds lemmas saying that ` HasSum f a` implies `HasProd (exp ∘ f) (exp a)` for `exp = rexp, cexp, NormedSpace.exp`. While the `rexp` and `cexp` versions could be deduced from the `NormedSpace.exp` one, we give a direct proof (and so avoid needing to import stuff about `NormedSpace.exp` for these results; the proofs are also a bit faster that way). Based on the discussion below, this also renames `Filter.Tendsto.exp` to `Filter.Tendsto.rexp` for the version specific to the real exponential function, so that `Filter.Tendsto.exp` can be used for the corresponding statement involving `NormedSpace.exp`. See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exp.28tsum.29.20.3D.20tprod.28exp.29/near/436891747) on Zulip. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

mathlib-bors · 2024-05-05T13:12:30Z

Pull request successfully merged into master.

Build succeeded:

This adds lemmas saying that ` HasSum f a` implies `HasProd (exp ∘ f) (exp a)` for `exp = rexp, cexp, NormedSpace.exp`. While the `rexp` and `cexp` versions could be deduced from the `NormedSpace.exp` one, we give a direct proof (and so avoid needing to import stuff about `NormedSpace.exp` for these results; the proofs are also a bit faster that way). Based on the discussion below, this also renames `Filter.Tendsto.exp` to `Filter.Tendsto.rexp` for the version specific to the real exponential function, so that `Filter.Tendsto.exp` can be used for the corresponding statement involving `NormedSpace.exp`. See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exp.28tsum.29.20.3D.20tprod.28exp.29/near/436891747) on Zulip. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

MichaelStollBayreuth added 3 commits April 24, 2024 22:36

perf: speed up slow number theory file

29360fc

Merge remote-tracking branch 'origin/master'

558cdc7

feat: add 'HasSum f a → HasProd (exp ∘ f) (exp a)'

84ed899

MichaelStollBayreuth added awaiting-review The author would like community review of the PR awaiting-CI t-analysis Analysis (normed *, calculus) labels May 3, 2024

revert inadvertent chages to RamificationInertia

9a48d69

github-actions bot removed the awaiting-CI label May 3, 2024

sgouezel reviewed May 4, 2024

View reviewed changes

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 4, 2024

MichaelStollBayreuth added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 4, 2024

MichaelStollBayreuth added 3 commits May 4, 2024 19:25

rename Filter.Tendsto.exp -> Filter.Tendsto.rexp

c3afd14

rename Filter.Tendsto.NormedSpace_exp -> Filter.Tendsto.exp

392ec7e

remove unncessary namespace

89eefaa

Ruben-VandeVelde reviewed May 4, 2024

View reviewed changes

Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 4, 2024

rename HasSum.NormedSpace_exp -> HasSum.exp

18b0f9b

MichaelStollBayreuth added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 4, 2024

Ruben-VandeVelde reviewed May 5, 2024

View reviewed changes

Mathlib/Analysis/SpecialFunctions/Exp.lean Show resolved Hide resolved

Update Mathlib/Analysis/SpecialFunctions/Exp.lean

2e79888

Ruben-VandeVelde approved these changes May 5, 2024

View reviewed changes

github-actions bot added the maintainer-merge label May 5, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 5, 2024

mathlib-bors bot changed the title ~~feat: add HasSum f a → HasProd (exp ∘ f) (exp a)~~ [Merged by Bors] - feat: add HasSum f a → HasProd (exp ∘ f) (exp a) May 5, 2024

mathlib-bors bot closed this May 5, 2024

mathlib-bors bot deleted the MS_exp_tsum branch May 5, 2024 13:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: add `HasSum f a → HasProd (exp ∘ f) (exp a)` #12635

[Merged by Bors] - feat: add `HasSum f a → HasProd (exp ∘ f) (exp a)` #12635

MichaelStollBayreuth commented May 3, 2024 •

edited

sgouezel May 4, 2024

MichaelStollBayreuth May 4, 2024

sgouezel May 4, 2024

MichaelStollBayreuth May 4, 2024

sgouezel May 4, 2024

MichaelStollBayreuth May 4, 2024

sgouezel May 4, 2024

MichaelStollBayreuth May 4, 2024

Ruben-VandeVelde May 4, 2024

MichaelStollBayreuth May 4, 2024

Ruben-VandeVelde May 4, 2024

MichaelStollBayreuth May 4, 2024

Ruben-VandeVelde May 4, 2024

Ruben-VandeVelde left a comment

github-actions bot commented May 5, 2024

sgouezel commented May 5, 2024

mathlib-bors bot commented May 5, 2024

mathlib-bors bot commented May 5, 2024

mathlib-bors bot commented May 5, 2024

[Merged by Bors] - feat: add HasSum f a → HasProd (exp ∘ f) (exp a) #12635

[Merged by Bors] - feat: add HasSum f a → HasProd (exp ∘ f) (exp a) #12635

Conversation

MichaelStollBayreuth commented May 3, 2024 • edited

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

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

github-actions bot commented May 5, 2024

sgouezel commented May 5, 2024

mathlib-bors bot commented May 5, 2024

mathlib-bors bot commented May 5, 2024

mathlib-bors bot commented May 5, 2024

[Merged by Bors] - feat: add `HasSum f a → HasProd (exp ∘ f) (exp a)` #12635

[Merged by Bors] - feat: add `HasSum f a → HasProd (exp ∘ f) (exp a)` #12635

MichaelStollBayreuth commented May 3, 2024 •

edited