Skip to content

Conversation

@eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Nov 12, 2023

This argument is still needed for almost all the lemmas, which means it can longer be found by unification.

We keep around expSeries 𝕂 A, as it's needed for talking about the radius of convergence over different base fields.

This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\

Zulip thread: #mathlib4 > Real.exp @ 💬


Open in Gitpod

This is started from the mathport output on leanprover-community/mathlib3#19244

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 12, 2023
@eric-wieser eric-wieser added awaiting-review awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. RFC Request for comment and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Nov 12, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 13, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Nov 13, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 5, 2024
eric-wieser added a commit that referenced this pull request Jan 5, 2024
…ditive monoids

While many of the lemmas cease to apply,
the definitions of sequences and their sums are still perfectly well-behaved in additive monoids;
no negation is needed.

We could use this to generalize `NormedSpace.exp` such that it works with `NNReal`,
but unless leanprover-community/mathlib3#16554 or similar lands and provides a `DivisionSemiring.nnqsmul` field,
that would conflict with #8370.
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 7, 2024
Copy link
Collaborator

@girving girving left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm curious if 𝕂 can be stripped from more of the lemmas, using the fact that any normed algebra is a real normed algebra. But possibly that would interfere with inference in practice?

analyticAt_exp_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
#align exp_analytic NormedSpace.exp_analytic

variable (𝕂)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need this? If it's so that we pull in a NormedAlgebra assumption, couldn't we always do that over the reals (since complex normed algebras are real normed algebras)?

[∀ i, NormedAlgebra 𝕂 (𝔸 i)] [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i) (i : ι) :
exp 𝕂 x i = exp 𝕂 (x i) :=
map_exp _ (Pi.evalRingHom 𝔸 i) (continuous_apply _) x
[∀ i, Algebra ℚ (𝔸 i)] [∀ i, NormedAlgebra 𝕂 (𝔸 i)] [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we switched the normed algebra to be always over the reals, as complex normed algebras are real normed algebras (resp. below)?

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 22, 2024
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 3, 2025
@github-actions
Copy link

github-actions bot commented Apr 3, 2025

PR summary 36187df13d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ expSeries_eq_expSeries_rat
+ expSeries_sum_eq_rat
+-+- exp_neg
+-+- exp_nsmul
+-+- exp_zsmul
+-+- isUnit_exp
- exp_eq_exp
- exp_ℝ_ℂ_eq_exp_ℂ_ℂ

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@eric-wieser eric-wieser removed the RFC Request for comment label Apr 3, 2025
@eric-wieser
Copy link
Member Author

eric-wieser commented Apr 3, 2025

I think there's a good chance a few of the instance hypotheses can be removed (in particular, anything that uses IsROrC can probably just use reals), but that's fine to put off.

I agree with this in theory; I guess the question is whether this ends up in annoying situations where NormedAlgebra Real A is not a global instance, but NormedAlgebra 𝕂 A is. I'd prefer to leave this to a follow-up. As is, the interface isn't too bad.

Copy link
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure about this. The addition of Algebra ℚ A assumptions is unpleasant, along with needing to remember to supply the 𝕜 argument to lemmas because it can't determine it from the type.

variable {A : Type*} [NormedRing A] [StarRing A]
[IsTopologicalRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
[ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [Algebra ℚ A]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yeah, I was worried about this kind of thing. It's going to be really annoying if, whenever we want to talk about the exponential in a C⋆-algebra, we have to add an Algebra ℚ A assumption.

@YaelDillies
Copy link
Collaborator

Can you explain in the PR description why mathematically you can remove the field argument?

@urkud urkud added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Apr 8, 2025
@leanprover-community-bot-assistant
Copy link
Collaborator

This pull request has conflicts, please merge master and resolve them.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 13, 2025
@urkud
Copy link
Member

urkud commented Apr 25, 2025

Can you explain in the PR description why mathematically you can remove the field argument?

Thanks for the question! It motivated me to find ratCast_smul_eq. This means that we can define the exponent using something like if \exists (K : Type) (_ : DivisionRing K), Nonempty (Module K A) then (use choice) else 1 and have equality for any (L : Type*) [DivisionRing L] [Module L A]. @eric-wieser wdyt? UPD: there is another "use Classical.choice" proposal on Zulip, left my comments there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

10 participants