## Stream: new members

### Topic: Kepler's Third Law

#### Adhithi Varadarajan⚛️ (Jul 31 2023 at 18:06):

Hello everyone, I was trying to prove Kepler's Law using Newtonian mechanics. Could you help me fill the sorry using tactics?

import Mathlib.Data.Real.Sqrt
import Mathlib.Algebra.Algebra.Pi

open Real

example {m_1 m_2 d_1 d_2 d w F_g F_c p : }
(h1 : m_1*d_1 = m_2*d_2) -- Center of mass
(h2 : d = d_1 + d_2 ) -- Distance between two bodies
(h3 : F_g = G*m_1*m_2/d^2) -- Gravitational Force
(h4 : F_c=  m_2*d_2*w^2 ) -- Centrifugal Force
(h5 : F_c = F_g) -- Force Balance
(h6 : p = 2*π/w) -- Period definition
-- m_1>0 , m_2>0, d_1>0, d_2>0, p>0 {Positivity constraints}
(h7 : m_1>0)
(h8 : m_2>0)
(h9 : d_1>0)
(h10 : d_2 >0)
(h11: p>0) :
p= Real.sqrt ((4* π^2*d^3)/(G*(m_1+ m_2))) :=
calc
p = (2*π/w) := by rw[h6]
_= Real.sqrt ((2*π/w)^2) := sorry
_= Real.sqrt ((4*π^2)/w^2) := by ring_nf
-- w^2= F_c/(m_2*d_2) from h4
_= Real.sqrt ((4*π^2)/(F_c/m_2*d_2)) := by sorry
_= Real.sqrt ((4*π^2*m_2*d_2)/F_c) := by sorry
_= Real.sqrt ((4*π^2*m_2*d_2)/F_g) := by rw[h5]
_= Real.sqrt ((4*π^2*m_2*d_2*d^2)/(G*m_1*m_2)) := by sorry
_= Real.sqrt ((4*π^2*d_2*d^2)/(G*m_1)) := by sorry
_= Real.sqrt ((4*π^2*d^2)/(G*(m_1/d_2))) := by sorry
_= Real.sqrt ((4*π^2*d^2*(d_1+d_2))/(G*(m_1/d_2)*(d_1+d_2))) := by sorry
_= Real.sqrt ((4*π^2*d^2*(d_1+d_2))/(G*((m_1*d_1/d_2)+m_1))) := by sorry
_= Real.sqrt ((4*π^2*d^2*(d_1 + d_2))/(G*(m_2+m_1))) := by sorry
_= Real.sqrt ((4*π^2*d^2*d)/(G*(m_1+m_2))) := by sorry
_= Real.sqrt ((4*π^2*d^3)/(G*(m_1 +m_2))) := by ring_nf

#### Eric Wieser (Jul 31 2023 at 18:12):

I think the third sorry is false

#### Eric Wieser (Jul 31 2023 at 18:12):

F_c/(m_2*d_2) is not the same as F_c/m_2*d_2

#### Eric Wieser (Jul 31 2023 at 18:13):

field_simp; ring can probably make progress on a lot of them

#### Jireh Loreaux (Jul 31 2023 at 18:16):

Also, a have : w ^ 2 = G * (m_1 + m_2) / (d ^ 3) would remove a lot of the noise here.

#### Jireh Loreaux (Jul 31 2023 at 18:17):

(or 1 / w ^ 2 = d ^ 3 / (G * (m_1 + m_3)) if you prefer.)

#### Adhithi Varadarajan⚛️ (Jul 31 2023 at 19:00):

Eric Wieser said:

I think the third sorry is false

Yes, that's correct. I have made the changes. Thanks for pointing it out.

#### Scott Morrison (Aug 01 2023 at 07:19):

You should do the elliptical orbit case too! :-) It would be lovely to have the proof that trajectories under an inverse square law are conic sections.

Last updated: Dec 20 2023 at 11:08 UTC