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[bot]]

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'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[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style