Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: use Qq in new Gamma positivity extension #7900

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore: use Qq in new Gamma positivity extension #7900

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8487439
chore: use Qq in new Gamma positivity function
dwrensha Oct 24, 2023
9c948a8
apply simplification suggested by alexjbest
dwrensha Oct 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 6 additions & 8 deletions Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -543,15 +543,13 @@ open Lean.Meta Qq in
/-- The `positivity` extension which identifies expressions of the form `Gamma a`. -/
@[positivity Gamma (_ : ℝ)]
def _root_.Mathlib.Meta.Positivity.evalGamma :
Mathlib.Meta.Positivity.PositivityExt where eval {_ _α} zα pα e := do
let (.app _ (a : Q($_α))) ← withReducible (whnf e) | throwError "not Gamma ·"
Mathlib.Meta.Positivity.PositivityExt where eval {_ _α} zα pα (e : Q(ℝ)) := do
let ~q(Gamma $a) := e | throwError "failed to match on Gamma application"
match ← Mathlib.Meta.Positivity.core zα pα a with
| .positive pa =>
let pa' ← mkAppM ``Gamma_pos_of_pos #[pa]
pure (.positive pa')
| .nonnegative pa =>
let pa' ← mkAppM ``Gamma_nonneg_of_nonneg #[pa]
pure (.nonnegative pa')
| .positive (pa : Q(0 < $a)) =>
pure (.positive (q(Gamma_pos_of_pos $pa) : Q(0 < $e)))
| .nonnegative (pa : Q(0 ≤ $a)) =>
pure (.nonnegative (q(Gamma_nonneg_of_nonneg $pa) : Q(0 ≤ $e)))
| _ => pure .none

/-- The Gamma function does not vanish on `ℝ` (except at non-positive integers, where the function
Expand Down
Loading