hamiltonian_energy_conservedtheoremProved here from basic factspropext, Classical.choice, Quot.sound
hamiltonian_energy_conservedLean 4Proved here from basic factsFormally verified
/-- **Hamiltonian flows conserve the Hamiltonian.** Let `ω` be any alternating form on a realnormed space `V` (`ω v v = 0`), `H : V → ℝ` differentiable with derivative `dH z` at `z`, and `X`the Hamiltonian vector field, defined by `ι_{X} ω = dH`, i.e. `ω (X z) w = dH z w`. Along anyflow line `γ' = X(γ)` the value `H(γ t)` is constant. Proof: by the chain rule`(H ∘ γ)' = dH(γ)(X(γ)) = ω(X(γ), X(γ)) = 0`. Non-degeneracy of `ω` is what makes `X` exist andbe unique; it is not needed for conservation. -/theorem hamiltonian_energy_conserved {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : V → V → ℝ) (hω : ∀ v, ω v v = 0) {H : V → ℝ} {dH : V → V →L[ℝ] ℝ} (hH : ∀ z, HasFDerivAt H (dH z) z) {X : V → V} (hX : ∀ z w, ω (X z) w = dH z w) {γ : ℝ → V} (hγ : ∀ t, HasDerivAt γ (X (γ t)) t) (s t : ℝ) : H (γ s) = H (γ t) := by have hd : ∀ τ, HasDerivAt (fun τ => H (γ τ)) 0 τ := by intro τ have h := (hH (γ τ)).comp_hasDerivAt τ (hγ τ) have h0 : dH (γ τ) (X (γ τ)) = 0 := by rw [← hX, hω] rw [h0] at h exact h exact is_const_of_deriv_eq_zero (fun τ => (hd τ).differentiableAt) (fun τ => (hd τ).deriv) s t
transpose_mul_J2_multheoremProved here from basic factspropext, Classical.choice, Quot.sound
transpose_mul_J2_mulLean 4Proved here from basic factsFormally verified
/-- For every real 2 × 2 matrix, `Aᵀ J A = (det A) J`: a linear map of the plane multiplies thesymplectic form, i.e. signed area, by its determinant. Proved entry by entry. -/theorem transpose_mul_J2_mul (A : Matrix (Fin 2) (Fin 2) ℝ) : Aᵀ * J2 * A = A.det • J2 := by ext i j fin_cases i <;> fin_cases j <;> simp [J2, Matrix.mul_apply, Fin.sum_univ_two, Matrix.det_fin_two] <;> ring
symplectic_iff_det_eq_onetheoremProved here from basic factspropext, Classical.choice, Quot.sound
symplectic_iff_det_eq_oneLean 4Proved here from basic factsFormally verified
/-- **In dimension two, symplectic means area- and orientation-preserving**: `Aᵀ J A = J` ifand only if `det A = 1`. In dimension four and higher this fails (see `squeeze`). -/theorem symplectic_iff_det_eq_one (A : Matrix (Fin 2) (Fin 2) ℝ) : Aᵀ * J2 * A = J2 ↔ A.det = 1 := by rw [transpose_mul_J2_mul] constructor · intro h have := congrFun (congrFun h 0) 1 simpa [J2] using this · intro h rw [h, one_smul]
shear_symplectictheoremProved here from basic factspropext, Classical.choice, Quot.sound
shear_symplecticLean 4Proved here from basic factsFormally verified
/-- A shear `(q, p) ↦ (q + t p, p)` is symplectic: its determinant is `1`. (Solution of the Leanexercise; it also describes the exact flow of the free particle `H = p²/2` for time `t`.) -/theorem shear_symplectic (t : ℝ) : (!![1, t; 0, 1] : Matrix (Fin 2) (Fin 2) ℝ)ᵀ * J2 * !![1, t; 0, 1] = J2 := by rw [symplectic_iff_det_eq_one, Matrix.det_fin_two_of] ring
det_eq_zero_of_skew_oddtheoremProved here from basic factspropext, Classical.choice, Quot.sound
det_eq_zero_of_skew_oddLean 4Proved here from basic factsFormally verified
/-- A skew-symmetric real matrix of odd size is singular: `det A = det Aᵀ = det (-A) =(-1)ⁿ det A = -det A`. So an alternating bilinear form on an odd-dimensional space is alwaysdegenerate, and a symplectic vector space (or manifold) has even dimension. -/theorem det_eq_zero_of_skew_odd {n : ℕ} (hn : Odd n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : Aᵀ = -A) : A.det = 0 := by have h1 : A.det = (-A).det := by rw [← hA, det_transpose] rw [det_neg, Fintype.card_fin, hn.neg_one_pow] at h1 linarith
symplectic_transpose_memtheoremApplies a library theorempropext, Classical.choice, Quot.sound
symplectic_transpose_memLean 4Applies a library theoremFormally verified
/-- The transpose of a symplectic matrix is symplectic (so `A * J * Aᵀ = J` and `Aᵀ * J * A = J`define the same group). This applies Mathlib's `SymplecticGroup.transpose_mem`. It is why the*rows* of a symplectic matrix pair up under `ω`, which the non-squeezing proof below uses. -/theorem symplectic_transpose_mem {l : Type*} [DecidableEq l] [Fintype l] {A : Matrix (l ⊕ l) (l ⊕ l) ℝ} (hA : A ∈ symplecticGroup l ℝ) : Aᵀ ∈ symplecticGroup l ℝ := SymplecticGroup.transpose_mem hA
/-- The standard symplectic form on ℝ⁴: the sum of the signed areas of the projections of theparallelogram spanned by `u` and `v` to the `(x₁, y₁)`- and `(x₂, y₂)`-planes. -/def omega4 (u v : Fin 4 → ℝ) : ℝ := u 0 * v 1 - u 1 * v 0 + u 2 * v 3 - u 3 * v 2
mul_J4_mul_transpose_applytheoremProved here from basic factspropext, Classical.choice, Quot.sound
mul_J4_mul_transpose_applyLean 4Proved here from basic factsFormally verified
/-- The entries of `A J Aᵀ` are the symplectic pairings of the rows of `A`:`(A J Aᵀ)ᵢⱼ = ω₀(rowᵢ A, rowⱼ A)`. -/theorem mul_J4_mul_transpose_apply (A : Matrix (Fin 4) (Fin 4) ℝ) (i j : Fin 4) : (A * J4 * Aᵀ) i j = omega4 (A i) (A j) := by simp [J4, omega4, Matrix.mul_apply, Fin.sum_univ_four] ring
wirtinger4theoremProved here from basic factspropext, Classical.choice, Quot.sound
wirtinger4Lean 4Proved here from basic factsFormally verified
/-- **A Wirtinger-type inequality in ℝ⁴**: `ω₀(a, b)² + ⟨a, b⟩² ≤ |a|² |b|²`. The symplectic areaof a parallelogram never exceeds its Euclidean area. Proof: the difference is the sum of squares`(p₀₂ - p₁₃)² + (p₀₃ + p₁₂)²` of Plücker coordinates `pᵢⱼ = aᵢ bⱼ - aⱼ bᵢ` (an identity checkedby `ring`). -/theorem wirtinger4 (a b : Fin 4 → ℝ) : omega4 a b ^ 2 + (a ⬝ᵥ b) ^ 2 ≤ (a ⬝ᵥ a) * (b ⬝ᵥ b) := by have key : (a ⬝ᵥ a) * (b ⬝ᵥ b) - (omega4 a b ^ 2 + (a ⬝ᵥ b) ^ 2) = ((a 0 * b 2 - a 2 * b 0) - (a 1 * b 3 - a 3 * b 1)) ^ 2 + ((a 0 * b 3 - a 3 * b 0) + (a 1 * b 2 - a 2 * b 1)) ^ 2 := by simp only [dotProduct, Fin.sum_univ_four, omega4] ring nlinarith [sq_nonneg ((a 0 * b 2 - a 2 * b 0) - (a 1 * b 3 - a 3 * b 1)), sq_nonneg ((a 0 * b 3 - a 3 * b 0) + (a 1 * b 2 - a 2 * b 1))]
dot_self_nonnegtheoremProved here from basic factspropext, Classical.choice, Quot.sound
dot_self_nonnegLean 4Proved here from basic factsFormally verified
/-- `|a|² = ⟨a, a⟩ ≥ 0` in ℝ⁴: a sum of four squares. -/theorem dot_self_nonneg (a : Fin 4 → ℝ) : 0 ≤ a ⬝ᵥ a := by simp only [dotProduct, Fin.sum_univ_four] nlinarith [mul_self_nonneg (a 0), mul_self_nonneg (a 1), mul_self_nonneg (a 2), mul_self_nonneg (a 3)]
exists_long_shadowtheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_long_shadowLean 4Proved here from basic factsFormally verified
/-- If `|a| ≥ 1`, the linear function `u ↦ ⟨a, u⟩` takes a value of size at least `r` on thesphere of radius `r`: take `u = (r / |a|) a`, for which `⟨a, u⟩² = r² |a|² ≥ r²`. -/theorem exists_long_shadow {a : Fin 4 → ℝ} (ha : 1 ≤ a ⬝ᵥ a) {r : ℝ} : ∃ u : Fin 4 → ℝ, u ⬝ᵥ u = r ^ 2 ∧ r ^ 2 ≤ (a ⬝ᵥ u) ^ 2 := by set s := Real.sqrt (a ⬝ᵥ a) with hs have hs2 : s ^ 2 = a ⬝ᵥ a := Real.sq_sqrt (by linarith) have hspos : 0 < s := Real.sqrt_pos.mpr (by linarith) refine ⟨(r / s) • a, ?_, ?_⟩ · rw [smul_dotProduct, dotProduct_smul, smul_eq_mul, smul_eq_mul, ← hs2] field_simp · rw [dotProduct_smul, smul_eq_mul, mul_pow, div_pow, hs2] have h0 : 0 < a ⬝ᵥ a := by linarith rw [div_mul_eq_mul_div, le_div_iff₀ h0] nlinarith [mul_nonneg (sq_nonneg r) (mul_nonneg h0.le (sub_nonneg.mpr ha))]
linear_nonsqueezingtheoremProved here from basic factspropext, Classical.choice, Quot.sound
linear_nonsqueezingLean 4Proved here from basic factsFormally verified
/-- **Linear non-squeezing in ℝ⁴.** If a symplectic matrix `A` (here `A J Aᵀ = J`) maps the ball`B⁴(r)` into the cylinder `Z(R) = {x₁² + y₁² ≤ R²}`, then `r ≤ R`. Proof: the first two rows`a, b` of `A` satisfy `ω₀(a, b) = 1`, so by `wirtinger4` `|a|² |b|² ≥ 1` and one of them haslength at least `1`; `exists_long_shadow` then gives a point of `B⁴(r)` whose image lies atdistance at least `r` from the axis of the cylinder. Gromov's theorem says the same for allsymplectic *diffeomorphisms*; that needs pseudo-holomorphic curves and is not formalised. -/theorem linear_nonsqueezing (A : Matrix (Fin 4) (Fin 4) ℝ) (hA : A * J4 * Aᵀ = J4) {r R : ℝ} (hR : 0 ≤ R) (hsub : ∀ u : Fin 4 → ℝ, u ⬝ᵥ u ≤ r ^ 2 → (A *ᵥ u) 0 ^ 2 + (A *ᵥ u) 1 ^ 2 ≤ R ^ 2) : r ≤ R := by -- the rows `a = A 0` and `b = A 1` satisfy `ω(a, b) = 1` have hab : omega4 (A 0) (A 1) = 1 := by rw [← mul_J4_mul_transpose_apply, hA]; simp [J4] have hw := wirtinger4 (A 0) (A 1) rw [hab] at hw have ha0 := dot_self_nonneg (A 0) have hb0 := dot_self_nonneg (A 1) -- one of the two rows has length at least one have hlong : 1 ≤ A 0 ⬝ᵥ A 0 ∨ 1 ≤ A 1 ⬝ᵥ A 1 := by rcases le_or_gt 1 (A 0 ⬝ᵥ A 0) with h | h · exact Or.inl h · rcases le_or_gt 1 (A 1 ⬝ᵥ A 1) with h' | h' · exact Or.inr h' · nlinarith [sq_nonneg (A 0 ⬝ᵥ A 1), mul_le_mul h.le h'.le hb0 zero_le_one] -- so some point of the ball lands at distance ≥ r from the axis have hr2 : r ^ 2 ≤ R ^ 2 := by rcases hlong with h | h · obtain ⟨u, hu, hshadow⟩ := exists_long_shadow h (r := r) have := hsub u hu.le simp only [mulVec] at this nlinarith [sq_nonneg (A 1 ⬝ᵥ u)] · obtain ⟨u, hu, hshadow⟩ := exists_long_shadow h (r := r) have := hsub u hu.le simp only [mulVec] at this nlinarith [sq_nonneg (A 0 ⬝ᵥ u)] nlinarith
squeeze_not_symplectictheoremProved here from basic factspropext, Classical.choice, Quot.sound
squeeze_not_symplecticLean 4Proved here from basic factsFormally verified
/-- The squeeze is not symplectic: it multiplies `ω₀(e₁, e₂) = 1` by `¼`. -/theorem squeeze_not_symplectic : squeeze * J4 * squeezeᵀ ≠ J4 := by intro h have := congrFun (congrFun h 0) 1 simp [squeeze, J4, Matrix.mul_apply, Fin.sum_univ_four] at this norm_num at this
squeeze_balltheoremProved here from basic factspropext, Classical.choice, Quot.sound
squeeze_ballLean 4Proved here from basic factsFormally verified
/-- The squeeze maps the unit ball `B⁴(1)` into the thin cylinder `Z(1/2)`. Together with`linear_nonsqueezing` this shows that volume preservation is far weaker than being symplectic:no symplectic matrix can do this. -/theorem squeeze_ball (u : Fin 4 → ℝ) (hu : u ⬝ᵥ u ≤ 1) : (squeeze *ᵥ u) 0 ^ 2 + (squeeze *ᵥ u) 1 ^ 2 ≤ (1 / 2) ^ 2 := by simp only [squeeze, mulVec_diagonal] simp only [dotProduct, Fin.sum_univ_four] at hu simp nlinarith [sq_nonneg (u 2), sq_nonneg (u 3)]
/-- Show that the shear `(q, p) ↦ (q + t p, p)` is symplectic.Hint: rewrite with `symplectic_iff_det_eq_one`, then compute the determinant with`Matrix.det_fin_two_of`. -/theorem shear_symplectic (t : ℝ) : (!![1, t; 0, 1] : Matrix (Fin 2) (Fin 2) ℝ)ᵀ * J2 * !![1, t; 0, 1] = J2 := by sorry
Show the compiled solution
shear_symplecticLean 4Proved here from basic factsFormally verified
/-- A shear `(q, p) ↦ (q + t p, p)` is symplectic: its determinant is `1`. (Solution of the Leanexercise; it also describes the exact flow of the free particle `H = p²/2` for time `t`.) -/theorem shear_symplectic (t : ℝ) : (!![1, t; 0, 1] : Matrix (Fin 2) (Fin 2) ℝ)ᵀ * J2 * !![1, t; 0, 1] = J2 := by rw [symplectic_iff_det_eq_one, Matrix.det_fin_two_of] ring