chore: add tag fun_prop to MeromorphicOn and AnalyticOnNhd - #42570
Open
kebekus wants to merge 7 commits into
Open
chore: add tag fun_prop to MeromorphicOn and AnalyticOnNhd#42570kebekus wants to merge 7 commits into
fun_prop to MeromorphicOn and AnalyticOnNhd#42570kebekus wants to merge 7 commits into
Conversation
`AnalyticAt` has been a registered `fun_prop` property for a while, but its set-relative sibling `AnalyticOnNhd` was not, even though every lemma needed to support it already existed. This registers the predicate and tags the lemmas that `fun_prop` needs: the identity and constant lambda theorems, the composition theorem, `Prod.mk`, and the arithmetic closure lemmas. Follows the pattern already established for `ContinuousOn` and `DifferentiableOn`: as for those, `AnalyticOnNhd` goals involving `inv`, `div` or a composition need `fun_prop (disch := ...)` to discharge the non-vanishing and `Set.MapsTo` side goals. `AnalyticOnNhd.pi` is deliberately left untagged, mirroring `AnalyticAt.pi`: its statement `fun x ↦ (f · x)` has the arguments in the opposite order to the one `fun_prop` recognises as a pi theorem. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…um` signatures
`MeromorphicOn.logDeriv` took its hypothesis as `{hf : MeromorphicOn f U}`,
i.e. implicit, so it could never be inferred and the lemma was unusable. Make it
explicit, matching `Meromorphic.logDeriv`.
`MeromorphicOn.fun_sum` required `∀ σ, MeromorphicOn (f σ) U` where the
point-free `MeromorphicOn.sum` and the corresponding `MeromorphicAt.fun_sum`
both require only `∀ σ ∈ s, ...`. Weaken the hypothesis to match.
Neither lemma had any call site in Mathlib, so this breaks nothing.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`MeromorphicAt.comp_analyticAt` states that the composition of a meromorphic function with an analytic one is meromorphic, but there was no `On`-level analogue. Add three: * `MeromorphicOn.comp_analyticOnNhd`, with a `Set.MapsTo` hypothesis, modelled on `ContinuousOn.comp'` and `DifferentiableOn.fun_comp`; * `MeromorphicOn.comp_analyticOnNhd_inter`, which trades that hypothesis for a smaller set, modelled on `ContinuousOn.comp_inter`; * `Meromorphic.comp_analyticOnNhd`, for a globally meromorphic outer function, modelled on `Continuous.comp_continuousOn'`. Note that the outer function must be the meromorphic one: the composition of an analytic function with a meromorphic one need not be meromorphic, as `fun z ↦ 1 / Complex.sin (π / z)` at `0` shows. Also add the missing `Meromorphic.id`, so that the `Meromorphic` namespace has both lambda theorems rather than just `Meromorphic.const`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`MeromorphicAt`, `Meromorphic` and `MeromorphicNFAt` have all been registered `fun_prop` properties for a while; `MeromorphicOn` was the remaining gap, so every `MeromorphicOn` goal had to be discharged by hand. Register the predicate and tag the closure lemmas, which already existed and already carried `to_fun`. Tagged: * the `def` itself, plus the `id` and `const` lambda theorems; * the arithmetic lemmas `add`, `sub`, `neg`, `smul`, `const_smul`, `mul`, `inv`, `div`, `pow`, `zpow` (switching `@[to_fun]` to `@[to_fun (attr := fun_prop)]`), the aggregates `sum`/`prod`/`finsum`/`finprod`, and `deriv`/`iterated_deriv`/ `logDeriv`; * the composition lemmas added in the previous commit; * the transitions `Meromorphic.meromorphicOn` and `AnalyticOnNhd.meromorphicOn`, mirroring `Continuous.continuousOn` and `Differentiable.differentiableOn`. The latter is what makes analytic leaves reachable from a `MeromorphicOn` goal, so `fun_prop` now proves e.g. `MeromorphicOn (fun z ↦ (z ^ 2 - 1)⁻¹) U`. Note that `MeromorphicOn.inv` and `.div` are unconditional, since `x⁻¹ = 0` for `x = 0` makes the identically-zero case analytic. So, unlike `DifferentiableOn`, meromorphic division needs no discharger. Also tag the leaves `Meromorphic.Gamma`, `MeromorphicOn.Gamma` and `meromorphic_digamma`: `fun_prop` previously could not prove anything at all about `Γ` or `ψ`. `tan`/`tanh` already carried `Meromorphic` tags and are now reachable for `MeromorphicOn` through the new transition. `MeromorphicOn.mono_set` is deliberately left untagged: the larger set is not determined by the goal, so unification cannot pick it. `ContinuousOn.continuousAt` is untagged for the same reason. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s, sinh, cosh The `AnalyticAt` versions of these were already tagged `@[fun_prop]`, but the `AnalyticOnNhd` versions were not, so `fun_prop` could not prove e.g. `AnalyticOnNhd ℂ Complex.sin U`. With `AnalyticOnNhd` now a registered `fun_prop` property this also makes these functions usable as leaves of a `MeromorphicOn` goal, through the `AnalyticOnNhd.meromorphicOn` transition: `fun_prop` now proves `MeromorphicOn (fun z ↦ Complex.exp z / (z ^ 2 - 1)) U`. Tagging alone was not enough for `exp`: `analyticOnNhd_cexp` and `analyticOnNhd_rexp` were stated only for `Set.univ`, so they could not match a goal over an arbitrary set. Generalise both to an arbitrary set; the existing call sites all still infer `univ`. The trigonometric and hyperbolic lemmas were already stated for an arbitrary set. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`MathlibTest/FunProp.lean` had two `MeromorphicAt` tests and nothing for `MeromorphicOn`, `Meromorphic` or the normal-form variants. Cover the newly registered `MeromorphicOn` property: the lambda theorems, arithmetic from hypotheses in context, `inv`/`div` needing no discharger, analytic leaves reached through the `AnalyticOnNhd` transition, both composition routes, `Finset.sum`, `logDeriv`, and `Γ`/`ψ`. Also add a `#guard_msgs` test pinning down that `fun_prop` fails on `MeromorphicOn (fun z ↦ Complex.exp (1 / z)) U`. This must keep failing: there is no general composition rule for meromorphic functions, since the composite of an analytic function with a meromorphic one need not be meromorphic. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Replace hand-written closure bookkeeping with `fun_prop` now that `MeromorphicOn` is a registered function property. The clearest case is in `MeromorphicOn.circleIntegrable_log_norm`, where five lines of `AnalyticOnNhd → MeromorphicOn` plumbing collapse to a single `fun_prop`. For that one, `analyticOnNhd_circleMap` had to be generalised from `Set.univ` to an arbitrary set and tagged, exactly as was done for `exp`; otherwise it cannot match a goal stated over an interval. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
PR summary 8d7db6e33aImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
Bot
added
the
t-measure-probability
kebekus
marked this pull request as ready for review
August 8, 2026 10:17
kebekus
added
t-analysis
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
For improved proof automation, add tag
fun_proptoMeromorphicOnandAnalyticOnNhd, provide transition lemmas, and golf existing call sites.