Complete the computable version of real.sqrt
#13634
Conversation
| lemma sq_div_self {a : ℚ} (a_nonzero : a ≠ 0) : a ^ 2 / a = a := | ||
| by rw [pow_two, div_eq_iff a_nonzero] |
There was a problem hiding this comment.
Note that the hypothesis is not needed given Lean's definition of division:
| lemma sq_div_self {a : ℚ} (a_nonzero : a ≠ 0) : a ^ 2 / a = a := | |
| by rw [pow_two, div_eq_iff a_nonzero] | |
| lemma sq_div_self {a : ℚ} : a ^ 2 / a = a := | |
| begin | |
| obtain rfl|a_nonzero := eq_or_ne a 0, | |
| { rw [div_zero] }, | |
| { rw [pow_two, div_eq_iff a_nonzero] } | |
| end |
and the lemma generalizes without changes to lemma sq_div_self {α : Type*} [group_with_zero α] {a : α} : a ^ 2 / a = a :=
| reduce the import graph. -/ | ||
| theorem rat.cauchy_schwarz (a b : ℚ) : 4 * a * b ≤ (a + b) ^ 2 := | ||
| begin | ||
| suffices pos: 0 ≤ (a + b) ^ 2 - 4 * a * b, exact sub_nonneg.mp pos, |
There was a problem hiding this comment.
| suffices pos: 0 ≤ (a + b) ^ 2 - 4 * a * b, exact sub_nonneg.mp pos, | |
| rw ←sub_nonneg, |
| { intros hyp, | ||
| { by_contradiction, | ||
| exact sqrt_aux_ne_zero_step f i h hyp, }, }, |
There was a problem hiding this comment.
| { intros hyp, | |
| { by_contradiction, | |
| exact sqrt_aux_ne_zero_step f i h hyp, }, }, | |
| { intros hyp, | |
| by_contradiction h, | |
| exact sqrt_aux_ne_zero_step f i h hyp, }, |
| induction i with i hyp, | ||
| { unfold sqrt_aux, exact zero_le_one}, | ||
| { unfold sqrt_aux, | ||
| simp, cancel_denoms, |
There was a problem hiding this comment.
You shouldn't leave a plain simp if it doesn't prove the goal - use simp? or squeeze_simp to replace it with simp only [...] with just the lemmas you use
src/data/real/sqrt.lean
Outdated
| ... ≤ sqrt_aux f i ^ 2 / 4 : div_nonneg (sq_nonneg _) (by norm_num), }, | ||
| { rw max_eq_right_of_lt h, | ||
| by_cases sqrt_aux f i = 0, | ||
| { simp at h, exfalso, exact h, }, |
There was a problem hiding this comment.
Maybe this will work:
| { simp at h, exfalso, exact h, }, | |
| { simpa using h }, |
src/data/real/sqrt.lean
Outdated
| by_cases sqrt_aux f i = 0, | ||
| { simp at h, exfalso, exact h, }, |
There was a problem hiding this comment.
Using by_cases and then immediately proving one case can't happen is not the most readable: you can do
have h : sqrt_aux f i ≠ 0,
{ ... },
src/data/real/sqrt.lean
Outdated
| by_cases sqrt_aux f i = 0, | ||
| { simp at h, exfalso, exact h, }, | ||
| { cancel_denoms, | ||
| have u : _ := rat.cauchy_schwarz (sqrt_aux f i ^ 2) (f (i + 1)), |
There was a problem hiding this comment.
| have u : _ := rat.cauchy_schwarz (sqrt_aux f i ^ 2) (f (i + 1)), | |
| have u := rat.cauchy_schwarz (sqrt_aux f i ^ 2) (f (i + 1)), |
|
Closing this because it's not obvious that it's even possible. The method doesn't converge at x=0, and I don't think diagonalising down to 0 is going to work either. |
This PR is dramatically not ready for merge, or even for review. I'm putting it up so that I have something to make the subject of an "anyone interested in this project" thread in Zulip.
It may or may not be useful to follow https://proofwiki.org/wiki/Hero%27s_Method.
I've redefined
sqrt_auxfrom what was originally there, because the original had some nasty "coalescing at 0" properties (see 430413a).