feat(ClassicalMechanics): SimplePendulum.periodFormula, the classical amplitude-dependent period - #1576
Conversation
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
adf0537 to
1b96a10
Compare
…ian and Hamilton's equations New module Physlib.ClassicalMechanics.Pendulum.SimplePendulum.Hamiltonian (imported from Physlib.lean), with the Hamiltonian formulation of the simple pendulum: - toCanonicalMomentum: the canonical momentum p = dL/dtheta-dot = I theta-dot, as a linear equivalence between velocities and momenta, with its value toCanonicalMomentum_eq. - hamiltonian: the Legendre transform of the Lagrangian, with hamiltonian_eq computing it as the momentum-space kinetic energy plus the potential energy, hamiltonian_contDiff for its joint smoothness, and the partial gradients gradient_hamiltonian_position_eq and gradient_hamiltonian_momentum_eq. - hamiltonian_eq_energy: along any lift of the angle the Hamiltonian, evaluated on the canonical momentum of the lift, is the energy. - hamiltonEqOp: the Hamilton-equations operator of the Hamiltonian on momentum-angle phase space. - equationOfMotion_iff_hamiltonEqOp_eq_zero: for a smooth lift of the angle the equation of motion is equivalent to Hamilton's equations. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Add section B to SimplePendulum/Hamiltonian.lean: equationOfMotion_tfae proves that, for a smooth lift of the angle, the pointwise equation of motion, the vanishing of the variational derivative of the action, Hamilton's equations, the Lagrangian variational principle and the Hamiltonian variational principle are all equivalent. Update the module doc (Key results bullet and TOC entry for section B) and the API map (Hamiltonian-formulation requirement row, Overview kept consistent). Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1b96a10 to
89d9627
Compare
|
I may have already said this, but just in case I haven't: if you want to get this stuff into the project quicker, you can use ./PhyslibAlpha, which has a quicker review process. If you're happy sitting through the review process for Physlib, that's also fine. Things that are in ./PhyslibAlpha will hopefully eventually be upstreamed to ./Physlib, and that is another process in itself. You're more than welcome to open your optic stuff if you want to merge this into Physlib as well - you don't have to wait for this review process to finish. |
…miltonian module - Rename `toCanonicalMomentum` to `canonicalMomentum` (the `to` prefix is for maps into a different type); `toCanonicalMomentum_eq` becomes `canonicalMomentum_eq`. - Inline the four one-line proofs of the linear equivalence. - Drop the sub-subsection heading that introduced a single lemma. Requested by review on leanprover-community#1570. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
… linearized equation of motion - toHarmonicOscillator (m := inertia, k := m g l) with simp projections and toHarmonicOscillator_omega - LinearizedEquationOfMotion with its Newton form (smoothness-free) and the equivalence with the oscillator's equation of motion for smooth lifts - imports HarmonicOscillator.Basic only (no Solution API used in this commit; the next commit extends the import) Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…m the harmonic oscillator - Import HarmonicOscillator.Solution (re-exporting Basic) to inherit the oscillator's solution theory. - smallAngleTrajectory: the small-angle motion of given initial conditions as the trajectory of the associated harmonic oscillator, with smoothness (smallAngleTrajectory_contDiff) and its initial data at time 0 (smallAngleTrajectory_at_zero, smallAngleTrajectory_velocity_at_zero). - Existence and uniqueness: smallAngleTrajectory_linearizedEquationOfMotion and linearized_unique, both transferred through linearizedEquationOfMotion_iff; uniqueness routes the separate initial-data hypotheses into the conjunction taken by HarmonicOscillator.InitialConditions.trajectories_unique. - releasedFromRest: the motion released from rest at angle θ₀ in the fun_prop-friendly cosine-smul shape, identified with the trajectory of ⟨single 0 θ₀, 0⟩ (releasedFromRest_eq), with its initial angle, vanishing initial angular velocity, and the linearized equation of motion. - Module doc: key results and table of contents extended for section C. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…y and the cubic linearization bound - Section D: smallAnglePeriod as the period of the associated harmonic oscillator, with the closed forms 2π/ω and 2π √(ℓ/g), positivity, the periodicity of every small-angle trajectory and of releasedFromRest, and the constant energy ½ (I ‖v₀‖² + m g ℓ ‖θ₀‖²) of a small-angle trajectory, transferred in its exact closed form from HarmonicOscillator.InitialConditions.trajectory_energy. - Section E: the cubic linearization bound |τ(θ) + m g ℓ θ| ≤ m g ℓ |θ|³/6 via Real.abs_sub_sin_le, the exact vector difference torque_sub_toHarmonicOscillator_force, and gradLagrangian_sub_toHarmonicOscillator identifying the difference of the variational gradients of the two actions with the difference of torque and linearized force, the inertial terms cancelling. - Task-2 review fold-ins: @[fun_prop] on smallAngleTrajectory_contDiff, @[simp] on the four at-zero lemmas, and the two small-angle docstring qualifiers; module doc ii/iii extended with the new sections. - API map: two new rows (the small-angle limit; the relation between the full and the linearized dynamics) and the overview clause brought up to date. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…ngle module - extend the Overview through the inherited solution theory, the mass- and amplitude-free period 2π√(ℓ/g), and the cubic measure of what the linearization discards - prose fixes: the pendulum "is approximated by" its associated oscillator; the released-from-rest periodicity docstring describes the linearized motion; the energy docstring names the initial angle as ‖IC.x₀‖ - Huygens: drop the historically inverted pendulum-clocks clause, keep the isochrony attribution, and add Horologium Oscillatorium (1673) to the references - state the rotational Newton form of the linearized equation with S.inertia - new lemmas: smallAngleTrajectory_eq (the closed form), norm_torque_sub_toHarmonicOscillator_force_le (the normed cubic bound), and norm_equationOfMotion_residual_le (new subsection E.3: a small-angle motion nearly solves the pendulum's own equation of motion) - reorder E.1 exact-difference-first and derive the coordinate bound from the exact difference instead of recomputing the torque - dot-notation for the associated oscillator's force and gradLagrangian sites - API map: the classical amplitude-dependent period formula follows in later modules; its identification with the nonlinear return time remains open Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…le limit, continuity and monotonicity in the amplitude - periodFormula θ₀ := 4 √(ℓ/g) completeEllipticK (sin² (θ₀/2)), the classical formula of Landau–Lifshitz §11 Problem 1 in the parameter convention, with a TODO listing the milestones toward identifying it with the period of the motion released from rest (uniqueness and time reversal are formalized in a companion module, contributed separately) - periodFormula_neg (evenness); periodFormula_zero = smallAnglePeriod (@[simp]) - continuousOn_periodFormula on (-π, π), continuousAt_periodFormula_zero, and the small-angle limit periodFormula_tendsto_smallAnglePeriod - periodFormula_mono / periodFormula_strictMono on 0 ≤ θ₁ ≤ θ₂ < π and their bundled forms monotoneOn_periodFormula / strictMonoOn_periodFormula on Set.Ico 0 π - the sandwich smallAnglePeriod_le_periodFormula ≤ … ≤ periodFormula_le / periodFormula_le' (smallAnglePeriod / cos (θ₀/2)), and periodFormula_pos - API-map rows: the formula (done) and the period theorem (done: false); Physlib.lean import Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
89d9627 to
b482c8a
Compare
|
Thanks — I'm happy to sit through the Physlib review for the pendulum series; the feedback has made the PRs better and the queue is moving. I'll take you up on the optics invitation separately: I'll start sending the first self-contained pieces of that once I've picked a sensible entry point, without waiting for these to finish. |
2 participants
Toward #883.
Stacked. Base is PR 5 (#1572,
b7bb4508); the commit belonging to this PR is the last one,b482c8a9(the module). #1573 (the elliptic integral) is merged, so this PR's own diff is
SimplePendulum/PeriodFormula.lean, onePhyslib.leanimport and two API-map rows. Review #1572 first.Defines the classical formula of Landau & Lifshitz, Mechanics, 3rd ed., §11 Problem 1 —
T = 4√(l/g) K(sin ½φ₀)in the modulus convention — as4 √(ℓ/g) · completeEllipticK (sin² (θ₀/2))in the parameter convention of #1573 (
m = k², Abramowitz & Stegun 17.3.1), and proves everythingthat follows from the theory of
Kalone.This PR does not claim that
periodFormula θ₀is the period of a solution. That identificationis not formalized; a
TODOafter the definition lists the remaining milestones (uniqueness andtime-reversal symmetry are supplied by the existence/uniqueness PR), and the API map carries the
period theorem as a separate
done: falserequirement.b482c8a9— the period-formula module (SimplePendulum/PeriodFormula.lean, new)periodFormuladef:4 √(ℓ/g) K(sin² (θ₀/2)), the classical formula for the period of libration at amplitudeθ₀periodFormula_negperiodFormula_zero(@[simp])periodFormula 0 = smallAnglePeriod, fromK 0 = π/2continuousOn_periodFormula,continuousAt_periodFormula_zero(−π, π), and at zero amplitudeperiodFormula_tendsto_smallAnglePeriodTendsto periodFormula (𝓝 0) (𝓝 smallAnglePeriod)— the small-angle limitperiodFormula_mono,periodFormula_strictMono0 ≤ θ₁ ≤ θ₂ < πmonotoneOn_periodFormula,strictMonoOn_periodFormulaSet.Ico 0 πsmallAnglePeriod_le_periodFormula,periodFormula_possin² (θ₀/2) < 1periodFormula_le,periodFormula_le'≤ 2π √(ℓ/g) / cos (θ₀/2) = smallAnglePeriod / cos (θ₀/2)for `Also:
Physlib.leanimport (sorted) and twoSimplePendulum/API-map.yamlrows (the formula,done: true; the period theorem,done: false).Reviewer reading order. Module doc §i — especially the paragraph beginning "What this module
does not do…", which fixes the scope;
periodFormulaand theTODO; §A.1 (the domain lemmaReal.sin_half_sq_lt_one, from #1573'sMathematics/Trigonometry/SinSq.lean, and the junk-value remark) and §A.2 (continuity ⇒ the small-angle limit,connecting to #1572's
smallAnglePeriod); §B.1–B.2 (monotonicity and the bounds, all inheritedfrom #1573's theory of
K); the API-map diff. Uniqueness and time-reversal symmetry — the TODO'sfirst two milestones — are formalized in the companion existence/uniqueness PR #1575, not here.
Verification. Warning-free builds; every declaration depends only on
propext,Classical.choice,Quot.sound; fulllake build+ the linter battery pass; imports minimal; theformula checked against Landau–Lifshitz §11 Problem 1 by hand under
m = k² = sin²(θ₀/2)(thecitation itself verified by the author against the printed source).
Developed with assistance from AI; all mathematics and proofs were reviewed and verified to compile.