analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
https://github.com/math-comp/analysis/blob/f29e974417442500e6014fb78e369f2e194a1eaa/theories/lebesgue_integral.v#L3479-L3481
https://github.com/math-comp/analysis/blob/f29e974417442500e6014fb78e369f2e194a1eaa/theories/ftc.v#L900 @IshiguroYoshihiro
https://github.com/math-comp/analysis/blob/3cd35520dc1d14ef272e2c6a25f41a94582ab041/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v#L50 should maybe be addressed before issue #1552
They are coming from the PR on the sampling lemma PR #1240 @t6s ```coq Lemma bounded_image (T : Type) (K : numFieldType) (V : pseudoMetricNormedZmodType K) (E : T ->...
It is now in `simple_functions.v`.
https://github.com/math-comp/analysis/blob/3cd35520dc1d14ef272e2c6a25f41a94582ab041/theories/lebesgue_integral_theory/lebesgue_integral_approximation.v#L45 to enhance discoverability
##### Motivation for this change The same simplification should apply to (most of) the following lines: ``` $ grep -n --color 'unitfE' $(git ls-files | grep '\.v$') theories/charge.v:867: by apply/funext...
##### Motivation for this change Generalizes the instances on function types to dependent function types. The same generalization is happening in mathcomp (see https://github.com/math-comp/math-comp/pull/1256) and it needs to be done...
##### Motivation for this change Some properties of `exp_coeff`. ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to...
##### Motivation for this change This is experimental generalization of monotone_convergence. - a sequence which is nondecreasing not for all n but over some N. - a sequence which is...