Eisenstein series are mdifferentiable

[CBirkbeck]

We show that Eisenstein Series are MDifferentiable

• [x] depends on: #10377
• [x] depends on: #11244

---

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#10377~~
• ~~leanprover-community/mathlib4#11244~~ By Dependent Issues (🤖). Happy coding!

[CBirkbeck]

I'm not sure if there is a more general version of MDifferentiable_iff_extension_DifferentiableOn that we might want to add. I experimented with this, but couldn't quite get the setup right.

[CBirkbeck]

I ran lake exe shake --update but I don't know if I should have, I'll wait for an expert to say if this is ok.

[loefflerd]

No, that's the wrong thing: you should revert your changes to noshake.json and run lake exe shake --fix instead.

[CBirkbeck]

No, that's the wrong thing: you should revert your changes to noshake.json and run lake exe shake --fix instead.

I did that originally, but the fix meant a file wouldn't compile, so I went for the update route.

[loefflerd]

That's weird. If lake exe shake --fix is giving wrong results, I suggest that you restore the branch to the state it was in before you started the tree-shaking, and then report on zulip that the script is giving misleading output on this branch.

[loefflerd]

I have done some digging and I know what's causing this. Shall I push my fix?

[CBirkbeck]

I have done some digging and I know what's causing this. Shall I push my fix?

Sure it seems it doesn't like the file where the notation is defined. I guess one solution is to move the notation from ../Manifold to ../Topology?

[loefflerd]

Not quite. The issue is that notation declarations are visible to the parser, but invisible to shake (which only notices when the notation is used, not when it's defined).

I suggest the following in UpperHalfPlane.Topology:

• add the PartialHomeomorph import
• add the following definition:

  /-- A continuous section `ℂ → ℍ` of the natural inclusion map, bundled as a `PartialHomeomorph`. -/
  def ofComplex : PartialHomeomorph ℂ ℍ := (openEmbedding_coe.toPartialHomeomorph _).symm
  
  /-- Extend a function on `ℍ` arbitrarily to a function on all of `ℂ`. -/
  scoped[UpperHalfPlane] notation "↑ₕ" f => f ∘ ofComplex
  

Then shake won't complain, because it sees the def and accepts that as a reason to import PartialHomeomorph. I think it's useful anyway to give the section of the inclusion map a name: then we can formulate a lemma that it's continuous or mdifferentiable, etc.

[loefflerd]

Looks good to me now. If you're happy with it, please label with "awaiting review" and "awaiting CI", and I'll flag it for merging if the CI run passes.

[CBirkbeck]

done!

[loefflerd]

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[RemyDegenne]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style