Search results

chore: deprecate_module for Analysis/Matrix

delegatedThis pull request has been delegated to the PR author (or occasionally another non-maintainer).This pull request has been delegated to the PR author (or occasionally another non-maintainer).

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31229

#31229 In leanprover-community/mathlib4;

· themathqueen opened on Nov 3, 2025

feat: AnalyticWithinAt.eventually_analyticWithinAt

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31211

#31211 In leanprover-community/mathlib4;

· bwangpj opened on Nov 3, 2025

Show that <code>expNegInvGlue</code> is not analytic at <code>0</code>

enhancementNew feature or requestNew feature or request

good first issueGood for newcomersGood for newcomers

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open.

#31209 In leanprover-community/mathlib4;

· mcdoll opened on Nov 3, 2025

feat(Analysis): a closed convex set is the intersection of countably many half-spaces in a separable Banach space

new-contributorThis PR was made by a contributor with at most 5 merged PRs. Welcome to the community!This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 31180

#31180 In leanprover-community/mathlib4;

· CoolRmal opened on Nov 2, 2025

feat(Analysis): Taylor's theorem with the integral remainder

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 31176

#31176 In leanprover-community/mathlib4;

· mcdoll opened on Nov 2, 2025

feat(Analysis/Calculus): parametric integrals over smooth functions are smooth

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31141

#31141 In leanprover-community/mathlib4;

· peabrainiac opened on Nov 1, 2025

feat(Analysis/Fourier): introduce notation type class for the Fourier transform

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31115

#31115 In leanprover-community/mathlib4;

· mcdoll opened on Oct 31, 2025

feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 31114

#31114 In leanprover-community/mathlib4;

· mcdoll opened on Oct 31, 2025

feat(Analysis/Distribution): basic algebraic properties of functions of temperate growth

delegatedThis pull request has been delegated to the PR author (or occasionally another non-maintainer).This pull request has been delegated to the PR author (or occasionally another non-maintainer).

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31112

#31112 In leanprover-community/mathlib4;

· mcdoll opened on Oct 31, 2025

feat(Analysis/InnerProductSpace): fderiv of norm squared

awaiting-authorA reviewer has asked the author a question or requested changes.A reviewer has asked the author a question or requested changes.

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31085

#31085 In leanprover-community/mathlib4;

· mcdoll opened on Oct 30, 2025

feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31079

#31079 In leanprover-community/mathlib4;

· mcdoll opened on Oct 30, 2025

feat(Analysis/InnerProductSpace): extension to linear isometry equivalence

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open (in progress).

leanprover-community/mathlib4number 31076

#31076 In leanprover-community/mathlib4;

· mcdoll opened on Oct 29, 2025