Louis Wasserman
Louis Wasserman
Fixed it to #1471.
Much appreciated. I had just thought of this issue as a thing I noticed was missing, but today I note the interesting consequence that this may help with the 68th...
Oof. Just realized that also, of course, large meet-semilattices and join-semilattices currently assume top/bottom elements, which is of course not something that exists for the reals. I continue to think...
(Does having a top/bottom imply nice properties? Yes, but it implies nice properties that meet-semilattices etc. do not actually have in general; Wikipedia calls those bounded meet-semilattices etc.)
Not looking in detail yet, but this may be hard or may require classical axioms: in https://math.stackexchange.com/q/2905324/23995 other people seem to struggle heavily with proving Cauchy-Schwarz constructively. My first attempt...
I have an idea that'll need fourth roots, but I think it might work. I'm mostly writing this so I remember in the morning.
Interesting. I had managed to get to ∥u ∙ v∥² ∥u∥² ∥v∥² ≤ ∥u∥⁴ ∥v∥⁴, but the idea of adding an epsilon had not yet occurred to me.
I think the tricksy bit in that proof is in fact showing that `(∥x∥ + ε)⁻¹ * x` has magnitude at most 1, but I have some ideas on how...
It took a bit of work, but I got that figured out.
The missing lemma we didn't actually have was ``` exists-ℚ⁺-mul-le-one-ℝ⁰⁺ : {l : Level} (x : ℝ⁰⁺ l) → exists ℚ⁺ (λ q → le-prop-ℝ⁰⁺ (nonnegative-real-ℚ⁺ q *ℝ⁰⁺ x) one-ℝ⁰⁺)...