List view

Lebesgue differentiation for continuous functions

Status: Merged (completed).

math-comp/analysisnumber 972

#972 In math-comp/analysis;

· by zstone1 was closed on Aug 22, 2023

Convexity of powR

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1011

#1011 In math-comp/analysis;

· by hoheinzollern was closed on Oct 2, 2023

lee_addgt0Pr

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 992

#992 In math-comp/analysis;

· by affeldt-aist was closed on Aug 8, 2023

ln is concave

Status: Merged (completed).

math-comp/analysisnumber 990

#990 In math-comp/analysis;

· by affeldt-aist was closed on Aug 11, 2023

declare kseries as an s-finite kernel

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1004

#1004 In math-comp/analysis;

· by affeldt-aist was closed on Aug 7, 2023

simplify proof script, %type in notations

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1013

#1013 In math-comp/analysis;

· by affeldt-aist was closed on Aug 31, 2023

script simplification

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1012

#1012 In math-comp/analysis;

· by affeldt-aist was closed on Aug 22, 2023

Lebesgue measure 20230807

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1005

#1005 In math-comp/analysis;

· by affeldt-aist was closed on Aug 8, 2023

Fixes 1016 and 1017

Status: Merged (completed).

math-comp/analysisnumber 1022

#1022 In math-comp/analysis;

· by affeldt-aist was closed on Sep 27, 2023

Lemma gt0_ltr_powR

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1027

#1027 In math-comp/analysis;

· by hoheinzollern was closed on Oct 2, 2023

Hoelder's inequality

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 942

#942 In math-comp/analysis;

· by affeldt-aist was closed on Sep 14, 2023

lee_opp -> leeN2

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1016 In math-comp/analysis;

· by affeldt-aist was closed on Sep 27, 2023

implicits of measurable_fst/snd

Status: Closed (completed).

#1017 In math-comp/analysis;

· by affeldt-aist was closed on Sep 27, 2023