Kepler's Third Law

Stream: new members

[Adhithi Varadarajan⚛️]

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]

I think the third sorry is false

[Eric Wieser]

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

[Eric Wieser]

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

[Jireh Loreaux]

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

[Jireh Loreaux]

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

[Adhithi Varadarajan⚛️]

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]

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.