[Merged by Bors] - feat(ContinuousFunctionalCalculus): Define the real log based on the CFC

[dupuisf]

This PR defines CFC.log as cfc Real.log, and shows its basic properties, such as the fact that it's the inverse of NormedSpace.exp ℝ. Along the way, we also show that the exponential defined via the CFC is equal to NormedSpace.exp, which is defined via power series.

---

[github-actions]

PR summary ec1d025449

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog	1879

---

Declarations diff

+ NormedSpace.exp_continuousMap_eq
+ _root_.IsSelfAdjoint.log
+ cfc_add_const
+ cfc_const_add
+ complex_exp_eq_normedSpace_exp
+ exp_eq_normedSpace_exp
+ exp_log
+ log
+ log_algebraMap
+ log_exp
+ log_one
+ log_pow
+ log_smul
+ log_zero
+ real_exp_eq_normedSpace_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>

[dupuisf]

It feels like this lemma should belong with NormedSpace.exp, but none of those files have the right imports. #find_home tells me to put it in Mathlib.Analysis.NormedSpace.Spectrum, but that feels even more out of place than just leaving it here.

[j-loreaux]

It's very annoying that aesop won't prove (∀ x ∈ spectrum ℝ a, 0 < x) → ∀ x ∈ spectrum ℝ a, x ≠ 0, but I also don't think we can make ne_of_gt or its synonyms into an aesop lemma (they would match too much, and they are very unsafe). It would be nice if we had some automation to handle this.

It would also be nice to have ways to customize the fun_prop part of cfc_cont_tac after the fact, maybe with some options? We should think about this. Because it would be good to add the necessary details (like the x ≠ 0 bit above), and then set an option to make cfc_cont_tac do what we need it to, without forcing ourselves to manually apply fun_prop with special dischargers.

[dupuisf]

It's very annoying that aesop won't prove (∀ x ∈ spectrum ℝ a, 0 < x) → ∀ x ∈ spectrum ℝ a, x ≠ 0, but I also don't think we can make ne_of_gt or its synonyms into an aesop lemma (they would match too much, and they are very unsafe). It would be nice if we had some automation to handle this.

It would also be nice to have ways to customize the fun_prop part of cfc_cont_tac after the fact, maybe with some options? We should think about this. Because it would be good to add the necessary details (like the x ≠ 0 bit above), and then set an option to make cfc_cont_tac do what we need it to, without forcing ourselves to manually apply fun_prop with special dischargers.

Yes, we should think about this at some point. I think it's an instance of a much more general problem though: how do we automatize goals like ContinuousOn on an interval? If there are function compositions, we need a way to map the interval through the function composition and to show that some interval is contained in another. I don't think we have any tactic at the moment that can do this well.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style