Yury G. Kudryashov
Yury G. Kudryashov
How does `modify` behave if other fields depend on this one? A semi-offtopic idea. There is `.copy` function used many times in `mathlib` that updates data fields to propositionally (but...
IMHO we should have a proper `structure` for bundled measurable functions (like the one we have for `continuous_map`s.
@b-mehta I'm done with the proofs. Could you please add a module docstring? E.g., I don't know where did you get these `l135` names from.
Note that [the weighted mean inequality](https://leanprover-community.github.io/mathlib_docs/analysis/mean_inequalities.html#real.young_inequality_of_nonneg) applied to `w₁=r`, `w₂=1-r`, `p₁=(1+x)^r`, `p₂=1` gives one version of this inequality, and other versions follow by change of variables.
In `sympy` `cancel` works with a ratio of multivariate polynomials. Of course, the equality holds only if we cancel a non-zero factor.
I don't remember why I wanted this. I remember that I didn't use these instances in the final version, then abandoned this pr. We can close it if it leads...
Could you please merge `master`? Otherwise LGTM. @eric-wieser, do you want to have another look? BTW, why most lemmas take `(h : is_maximal _)`, not `[is_maximal _]`?
@eric-wieser What are your plans about this: discard? port to Lean 4?
LGTM but let's wait for one more pair of eyes: I don't want to make decisions about universe-related questions by myself.