Chris_Y (Jun 27 2023 at 14:35): Chris_Y (Jun 27 2023 at 14:35):Hi everyone,
My goal is the following:
I can use an existing theorem to show there exist odd positive integers x, y and z such that n = x^2+y^2+z^2 if n mod 8 = 3. However, I'd like to assume without loss of generality that x >= y >= z. This assumption is not given in the original theorem, I wonder if there is any efficient way to do this.
Thank you so much for the help!
Manuel Eberl (Jun 27 2023 at 15:09):The easiest way I see is to rewrite it as n = sum_list (map (λx. x^2) [x,y,z]) and then show that this is the same as sum_list (map (λx. x^2) (sort [x,y,z])) and then obtain values a, b, c such that [a,b,c] = sort [x,y,z].
Manuel Eberl (Jun 27 2023 at 15:10):Each of those steps should be doable with a few suitable library lemmas and help from sledgehammer. But depending on how much experience you have with Isabelle it could still be a bit tricky, so feel free to ask if you are stuck with any particular step.
Manuel Eberl (Jun 27 2023 at 15:10):(might be sensible to go through multisets to justify that the two sets are the same)
Manuel Eberl (Jun 27 2023 at 15:11):alternatively you could of course just do a case distinction; that should also work
Manuel Eberl (Jun 27 2023 at 15:12):That is, proving the stronger version of the theorem from the weaker one with a by (cases "x ≤ y"; cases "y ≤ z"; cases "x ≤ z") (auto simp: algebra_simps) or something like that (not sure if that's enough).
Chris_Y (Jun 27 2023 at 16:38):That works! Thank you so much :)
Last updated: Dec 21 2024 at 16:20 UTC