analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
##### Motivation for this change fixes #662 closes #672 ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers ##### Reminder to reviewers...
In the theory `normedtype.v`, we have the lemma `not_near_at_rightP`. The name contains the character `P`, but it states one-direct implication, not the equivalence. For me, this seems contradictory to the...
I found some lemmas about `GRing.opp` which is named `opp_ ...` or `... _opp`, not `oppr_ ...` or `... _oppr`. I suppose these may be for distinguish between `GRing.opp` for...
I am formalizing the cumulative distribution function and related lemmas in `Probability.v`. A possible candidate for the definition is: ``` Definition cdf d (T : measurableType d) (R : realType)...
Do we need to keep both? ``` Lemma at_pointE T (t : T) : at_point t = principal_filter t. Proof. by apply:funext=> S; apply: propext; split=> [? ? -> |...
since the condition is a `mem` and the goal refers more explicitly to `set`? https://github.com/math-comp/analysis/blob/899c14175215cd7f0942eae93321c23ea0a92d7e/classical/classical_sets.v#L514
https://github.com/math-comp/analysis/blob/1ab682517f25e7f661e3b6dee2453778a535260f/theories/measure.v#L3575 the measure `P` should not be implicit
##### Motivation for this change ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document) ##### Reminder to reviewers...
might be better done after the following issues are adressed - PR #1551 - PR #1554
https://github.com/math-comp/analysis/blob/1ab682517f25e7f661e3b6dee2453778a535260f/theories/lebesgue_integral_theory/lebesgue_integrable.v#L705-L706 `integrable_ltNy` seems more appropriate