Symplectic
Results named in Tau Ceti's TauCeti.Geometry.Symplectic modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremCauchy--Schwarz along a complex line#
For a compatible pair, the squares of the
components g(v, w) and ω(v, w) = g(J v, w) of w along the orthogonal pair v, J v add up
to at most g(v, v) g(w, w).
TauCeti.SymplecticForm.Compatible.sq_associatedBilinForm_add_sq_le.{u_1} {V : Type u_1}
[AddCommGroup V] [_root_.Module ℝ V] {ω : TauCeti.SymplecticForm V}
{J : TauCeti.AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
((ω.associatedBilinForm J) v) w ^ 2 + (fun v w => (ω.toBilinForm v) w) v w ^ 2 ≤
((ω.associatedBilinForm J) v) v * ((ω.associatedBilinForm J) w) w
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.Compatible.sq_associatedBilinForm_add_sq_le.
Sources
Used by 1
TheoremEuler's identity for the kinetic energy#
The kinetic energy is homogeneous of degree two
in the fibres, so the Euler vector field Z = p ∂_p satisfies dK(Z) = 2K = ‖p‖².
TauCeti.CotangentBundle.mvfderiv_kineticEnergy_vectorBundleEulerField.{u_1, u_2, u_3} {E : Type u_1}
[NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H]
{I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M]
[Bundle.RiemannianBundle fun x => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M]
[IsContMDiffRiemannianBundle I 1 E fun x => TangentSpace I x] (z : TauCeti.CotangentBundle I M) :
(d% (TauCeti.CotangentBundle.kineticEnergy I M) z) (TauCeti.vectorBundleEulerField I z) =
‖z.snd‖ ^ 2
Lean
Formalized in Tau Ceti as TauCeti.CotangentBundle.mvfderiv_kineticEnergy_vectorBundleEulerField.
Sources
Uses 1
TheoremHamilton's principle of stationary action#
For 2 ≤ n ≤ ∞, let q be C^n at every
point of [a, b] and let L be jointly C² along q. Then q is a stationary point of the
action of L among C^n variations with fixed endpoints between a and b exactly when it
solves the Euler–Lagrange equations d/dt ∂_v L(t, q, q') = ∂_q L(t, q, q') at every time strictly
between a and b.
TauCeti.isActionStationary_iff_eulerLagrange.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {a b : ℝ} {n : WithTop ℕ∞} {q : ℝ → E} (hn : 2 ≤ n)
(hn' : n ≤ ↑⊤) (hq : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ n q t)
(hL : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 2 (Function.uncurry L) (t, q t, deriv q t)) :
TauCeti.IsActionStationary n L q a b ↔
∀ t ∈ Set.uIoo a b,
HasDerivAt (fun s => fderiv ℝ (fun u => L s (q s, u)) (deriv q s))
(fderiv ℝ (fun y => L t (y, deriv q t)) (q t)) t
TheoremIntegrated Wirtinger inequality#
For a compatible pair, the integral of the positive symplectic area density is at most the energy.
TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineEnergy.{u_1, u_2} {X : Type u_1}
{V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [_root_.Module ℝ V]
{J : TauCeti.AlmostComplexStructure V} {ω : TauCeti.SymplecticForm V}
{μ : MeasureTheory.Measure X} {du : X → ℝ × ℝ →ₗ[ℝ] V} (hcompat : ω.Compatible J) :
∫⁻ (x : X),
ENNReal.ofReal
((fun v w => (ω.toBilinForm v) w) ((du x) TauCeti.stdComplexLineReal)
((du x) TauCeti.stdComplexLineImag)) ∂μ ≤
ω.stdComplexLineEnergy J du μ
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineEnergy.
Other forms
Integrated Wirtinger inequality on manifolds. Formalized in Tau Ceti as TauCeti.SmoothTwoForm.Compatible.lintegral_twoForm_le_stdComplexLineEnergy.
TauCeti.SmoothTwoForm.Compatible.lintegral_twoForm_le_stdComplexLineEnergy.{u_1, u_2, u_3}
{E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
[TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M]
[IsManifold I (↑⊤) M] {form : TauCeti.SmoothTwoForm I M}
{J : TauCeti.SmoothAlmostComplexStructure I M} (hcompat : form.Compatible J) (u : ℝ × ℝ → M)
(du : (z : ℝ × ℝ) → ℝ × ℝ →ₗ[ℝ] TangentSpace I (u z)) (μ : MeasureTheory.Measure (ℝ × ℝ)) :
∫⁻ (z : ℝ × ℝ),
ENNReal.ofReal
(TauCeti.SmoothBundleForm.eval₂ form (u z) ((du z) TauCeti.stdComplexLineReal)
((du z) TauCeti.stdComplexLineImag)) ∂μ ≤
form.stdComplexLineEnergy J u du μ
Integrated Wirtinger inequality, area form. Formalized in Tau Ceti as TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineArea.
TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineArea.{u_1, u_2} {X : Type u_1}
{V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [_root_.Module ℝ V]
{J : TauCeti.AlmostComplexStructure V} {ω : TauCeti.SymplecticForm V}
{μ : MeasureTheory.Measure X} {du : X → ℝ × ℝ →ₗ[ℝ] V} (hcompat : ω.Compatible J) :
∫⁻ (x : X),
ENNReal.ofReal
((fun v w => (ω.toBilinForm v) w) ((du x) TauCeti.stdComplexLineReal)
((du x) TauCeti.stdComplexLineImag)) ∂μ ≤
ω.stdComplexLineArea J du μ
Sources
Uses 1
TheoremThe Jacobi identity for the Poisson bracket#
For a nondegenerate closed form on a
finite-dimensional manifold and C² functions f, g, k,
{f, {g, k}} + {g, {k, f}} + {k, {f, g}} = 0.
TauCeti.SmoothTwoForm.IsNondegenerate.poissonBracket_jacobi.{u_1, u_2, u_3} {E : Type u_1}
{H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
{I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M]
{σ : TauCeti.SmoothTwoForm I M} {f g : M → ℝ} [FiniteDimensional ℝ E] (h : σ.IsNondegenerate)
(hσ : TauCeti.SmoothForm.IsClosed σ) {k : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f)
(hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g)
(hk : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 k) (x : M) :
σ.poissonBracket f (σ.poissonBracket g k) x + σ.poissonBracket g (σ.poissonBracket k f) x +
σ.poissonBracket k (σ.poissonBracket f g) x =
0
Lean
Formalized in Tau Ceti as TauCeti.SmoothTwoForm.IsNondegenerate.poissonBracket_jacobi.
Sources
TheoremKepler's third law#
Between two distinct turning points 0 < r₁ < r₂ of a Kepler orbit
with ℓ ≠ 0, the radial period is 2π √(m / κ) a^(3/2) for the semi-major axis
a = (r₁ + r₂) / 2.
TauCeti.kepler_radialPeriod {m κ ℓ E r₁ r₂ : ℝ} (hm : 0 < m) (hℓ : ℓ ≠ 0) (h₁ : 0 < r₁)
(hlt : r₁ < r₂) (hr₁ : 2 * m * (E + κ / r₁) = ℓ ^ 2 / r₁ ^ 2)
(hr₂ : 2 * m * (E + κ / r₂) = ℓ ^ 2 / r₂ ^ 2) :
TauCeti.radialPeriod m (fun r => -κ / r) ℓ E r₁ r₂ =
2 * Real.pi * √(m / κ) * ((r₁ + r₂) / 2) ^ (3 / 2)
Uses 1
TheoremLinear Darboux theorem#
Two symplectic vector spaces of the same finite dimension are linearly symplectomorphic.
TauCeti.SymplecticForm.exists_isSymplectomorphism.{u_1, u_2} {V : Type u_1} {W : Type u_2}
[AddCommGroup V] [_root_.Module ℝ V] [AddCommGroup W] [_root_.Module ℝ W] [FiniteDimensional ℝ V]
[FiniteDimensional ℝ W] (ω₁ : TauCeti.SymplecticForm V) (ω₂ : TauCeti.SymplecticForm W)
(hdim : Module.finrank ℝ V = Module.finrank ℝ W) : ∃ e, ω₁.IsSymplectomorphism ω₂ e
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.exists_isSymplectomorphism.
Sources
Uses 1 · Used by 1
TheoremNoether's theorem#
The derivative of a function f along the generated vector field Z_M
vanishes exactly when f Poisson-commutes with the component μ_Z of a moment map.
TauCeti.SmoothTwoForm.IsMomentMap.poissonBracket_eq_zero_iff.{u_1, u_2, u_3, u_4} {E : Type u_1}
{H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H]
{I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M]
{𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra ℝ 𝔤] {σ : TauCeti.SmoothTwoForm I M}
{a : TauCeti.InfinitesimalAction 𝔤 I M} {μ : M → Module.Dual ℝ 𝔤} [FiniteDimensional ℝ E]
(h : σ.IsMomentMap a μ) (hσ : σ.IsNondegenerate) (f : M → ℝ) (Z : 𝔤) :
σ.poissonBracket (fun y => (μ y) Z) f = 0 ↔ ∀ (x : M), (d% f x) (a Z x) = 0
Lean
Formalized in Tau Ceti as TauCeti.SmoothTwoForm.IsMomentMap.poissonBracket_eq_zero_iff.
Other forms
Noether's theorem, pointwise in time. Formalized in Tau Ceti as TauCeti.hasDerivAt_noetherCharge.
TauCeti.hasDerivAt_noetherCharge.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
{L : ℝ → E × E → ℝ} {ξ : ℝ × E → E} {B : ℝ × E → ℝ} {q v : ℝ → E} {t : ℝ}
(hq : HasDerivAt q (v t) t)
(hEL :
HasDerivAt (fun s => fderiv ℝ (fun u => L s (q s, u)) (v s))
(fderiv ℝ (fun y => L t (y, v t)) (q t)) t)
(hL : DifferentiableAt ℝ (L t) (q t, v t)) (hξ : DifferentiableAt ℝ ξ (t, q t))
(hB : DifferentiableAt ℝ B (t, q t))
(hsym : TauCeti.lagrangianVariation L ξ t (q t, v t) = (fderiv ℝ B (t, q t)) (1, v t)) :
HasDerivAt (fun s => TauCeti.noetherCharge L ξ B s (q s, v s)) 0 t
Noether's theorem. Formalized in Tau Ceti as TauCeti.noetherCharge_eq_of_eulerLagrange.
TauCeti.noetherCharge_eq_of_eulerLagrange.{u_1} {E : Type u_1} [NormedAddCommGroup E]
[NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {ξ : ℝ × E → E} {B : ℝ × E → ℝ} {q v : ℝ → E} {s : Set ℝ}
(hs : IsOpen s) (hs' : IsPreconnected s) (hq : ∀ t ∈ s, HasDerivAt q (v t) t)
(hEL :
∀ t ∈ s,
HasDerivAt (fun s => fderiv ℝ (fun u => L s (q s, u)) (v s))
(fderiv ℝ (fun y => L t (y, v t)) (q t)) t)
(hL : ∀ t ∈ s, DifferentiableAt ℝ (L t) (q t, v t)) (hξ : ∀ t ∈ s, DifferentiableAt ℝ ξ (t, q t))
(hB : ∀ t ∈ s, DifferentiableAt ℝ B (t, q t))
(hsym : ∀ t ∈ s, TauCeti.lagrangianVariation L ξ t (q t, v t) = (fderiv ℝ B (t, q t)) (1, v t))
{t₀ t₁ : ℝ} (h₀ : t₀ ∈ s) (h₁ : t₁ ∈ s) :
TauCeti.noetherCharge L ξ B t₀ (q t₀, v t₀) = TauCeti.noetherCharge L ξ B t₁ (q t₁, v t₁)
Sources
TheoremThe relative Darboux theorem in adapted coordinates#
Let ω₀, ω₁ be closed C^r
two-forms (r ≥ 1) on an open subset W of E × N containing (q₀, 0), both nondegenerate at
(q₀, 0), with the same pullback to the zero section E × {0}. Then some C^r diffeomorphism ψ
of E × N fixes every point (q, 0) with q near q₀ and pulls ω₁ back to ω₀ near (q₀, 0).
The pullback to the zero section may be degenerate, of any rank.
TauCeti.exists_diffeomorph_fix_zeroSection_eventually_compContinuousLinearMap_fderiv_eq.{u_1, u_2}
{E : Type u_1} {N : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
[NormedAddCommGroup N] [NormedSpace ℝ N] [FiniteDimensional ℝ N]
{ω₀ ω₁ : E × N → (E × N) [⋀^Fin 2]→L[ℝ] ℝ} {W : Set (E × N)} {q₀ : E} {r : ℕ∞} (hr : 1 ≤ r)
(hW : IsOpen W) (hq₀ : (q₀, 0) ∈ W) (hω₀ : ContDiffOn ℝ (↑r) ω₀ W) (hω₁ : ContDiffOn ℝ (↑r) ω₁ W)
(hdω₀ : ∀ x ∈ W, extDeriv ω₀ x = 0) (hdω₁ : ∀ x ∈ W, extDeriv ω₁ x = 0)
(htan :
∀ (q : E),
(q, 0) ∈ W →
(ω₁ (q, 0)).compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N) =
(ω₀ (q, 0)).compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N))
(hnd₀ : ∀ (v : E × N), (∀ (w : E × N), (ω₀ (q₀, 0)) ![v, w] = 0) → v = 0)
(hnd₁ : ∀ (v : E × N), (∀ (w : E × N), (ω₁ (q₀, 0)) ![v, w] = 0) → v = 0) :
∃ ψ,
(∀ᶠ (q : E) in nhds q₀, ψ (q, 0) = (q, 0)) ∧
∀ᶠ (x : E × N) in nhds (q₀, 0), (ω₁ (ψ x)).compContinuousLinearMap (fderiv ℝ (⇑ψ) x) = ω₀ x
Lean
Formalized in Tau Ceti as TauCeti.exists_diffeomorph_fix_zeroSection_eventually_compContinuousLinearMap_fderiv_eq.
Sources
Uses 3
TheoremStokes' formula for symplectic area on an annulus#
The pullback area of a C² map is
the outer boundary action minus the inner boundary action for the primitive λₓ(v) = ½ ω(x, v).
This identity does not require any regularity on the inner disc or a holomorphicity hypothesis.
TauCeti.SymplecticForm.integral_fderiv_apply_annulus.{u_1} {V : Type u_1} [NormedAddCommGroup V]
[NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : TauCeti.SymplecticForm V) {u : ℂ → V} (z₀ : ℂ)
{a b : ℝ} (ha : 0 < a) (hab : a ≤ b)
(hu : ∀ z ∈ {z | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 2 u z) :
∫ (z : ℂ) in {z | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b},
(fun v w => (ω.toBilinForm v) w) ((fderiv ℝ u z) 1) ((fderiv ℝ u z) Complex.I) =
1 / 2 *
((∫ (θ : ℝ) in -Real.pi..Real.pi,
(fun v w => (ω.toBilinForm v) w) (u (circleMap z₀ b θ))
(deriv (fun θ => u (circleMap z₀ b θ)) θ)) -
∫ (θ : ℝ) in -Real.pi..Real.pi,
(fun v w => (ω.toBilinForm v) w) (u (circleMap z₀ a θ))
(deriv (fun θ => u (circleMap z₀ a θ)) θ))
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.integral_fderiv_apply_annulus.
Other forms
Stokes' formula for symplectic area on a rectangle. Formalized in Tau Ceti as TauCeti.SymplecticForm.integral_fderiv_apply_prod_Icc.
TauCeti.SymplecticForm.integral_fderiv_apply_prod_Icc.{u_1} {V : Type u_1} [NormedAddCommGroup V]
[NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : TauCeti.SymplecticForm V) {u : ℝ × ℝ → V}
{a b : ℝ × ℝ} (hle : a ≤ b) (hu : ∀ z ∈ Set.Icc a b, ContDiffAt ℝ 2 u z) :
∫ (z : ℝ × ℝ) in Set.Icc a b,
(fun v w => (ω.toBilinForm v) w) ((fderiv ℝ u z) (1, 0)) ((fderiv ℝ u z) (0, 1)) =
1 / 2 *
(((∫ (t : ℝ) in a.2..b.2,
(fun v w => (ω.toBilinForm v) w) (u (b.1, t)) ((fderiv ℝ u (b.1, t)) (0, 1))) -
∫ (t : ℝ) in a.2..b.2,
(fun v w => (ω.toBilinForm v) w) (u (a.1, t)) ((fderiv ℝ u (a.1, t)) (0, 1))) -
((∫ (s : ℝ) in a.1..b.1,
(fun v w => (ω.toBilinForm v) w) (u (s, b.2)) ((fderiv ℝ u (s, b.2)) (1, 0))) -
∫ (s : ℝ) in a.1..b.1,
(fun v w => (ω.toBilinForm v) w) (u (s, a.2)) ((fderiv ℝ u (s, a.2)) (1, 0))))
Stokes' formula for symplectic area on the truncated thrice-punctured sphere. Formalized in Tau Ceti as TauCeti.SymplecticForm.integral_fderiv_apply_truncation.
TauCeti.SymplecticForm.integral_fderiv_apply_truncation.{u_1} {V : Type u_1} [NormedAddCommGroup V]
[NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : TauCeti.SymplecticForm V) {u : ℂ → V}
(hu : ContDiffOn ℝ 2 u {w | w ≠ 0 ∧ w ≠ 1}) {R : ℝ} (hR : 1 ≤ R) :
∫ (w : ℂ) in TauCeti.ThricePuncturedSphere.truncation R,
(fun v w => (ω.toBilinForm v) w) ((fderiv ℝ u w) 1) ((fderiv ℝ u w) Complex.I) =
∑ q,
q.endSign * ω.loopArea fun t => u (q.cylindricalEndLift (↑(q.endSign * R) + ↑t * Complex.I))
Stokes' formula on a finite-energy punctured disc. Formalized in Tau Ceti as TauCeti.SymplecticForm.integral_fderiv_apply_punctured_disc.
TauCeti.SymplecticForm.integral_fderiv_apply_punctured_disc.{u_1} {V : Type u_1}
[NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : TauCeti.SymplecticForm V)
{u : ℂ → V} (z₀ : ℂ) {b : ℝ} (hb : 0 < b)
(hu : ∀ z ∈ {z | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 2 u z)
(henergy :
MeasureTheory.IntegrableOn (fun z => ‖fderiv ℝ u z‖ ^ 2) {z | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}
MeasureTheory.volume) :
∫ (z : ℂ) in {z | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b},
(fun v w => (ω.toBilinForm v) w) ((fderiv ℝ u z) 1) ((fderiv ℝ u z) Complex.I) =
1 / 2 *
∫ (θ : ℝ) in -Real.pi..Real.pi,
(fun v w => (ω.toBilinForm v) w) (u (circleMap z₀ b θ))
(deriv (fun θ => u (circleMap z₀ b θ)) θ)
Sources
Uses 2
TheoremVieta's formula for the Kepler sum of turning points#
If r₁ ≠ r₂ are nonzero turning
points of a Kepler orbit with m ≠ 0, then κ = -E (r₁ + r₂); equivalently, for E ≠ 0 the
semi-major axis (r₁ + r₂) / 2 is κ / (-2 E).
TauCeti.kepler_kappa_eq {m κ ℓ E r₁ r₂ : ℝ} (hm : m ≠ 0) (h₁ : r₁ ≠ 0) (h₂ : r₂ ≠ 0) (hne : r₁ ≠ r₂)
(hr₁ : 2 * m * (E + κ / r₁) = ℓ ^ 2 / r₁ ^ 2) (hr₂ : 2 * m * (E + κ / r₂) = ℓ ^ 2 / r₂ ^ 2) :
κ = -E * (r₁ + r₂)
Lean
Formalized in Tau Ceti as TauCeti.kepler_kappa_eq.
Other forms
Vieta's formula for the isotropic oscillator, product of squared turning points. Formalized in Tau Ceti as TauCeti.isotropicOscillator_sq_eq_sq_mul.
TauCeti.isotropicOscillator_sq_eq_sq_mul {m ν ℓ E r₁ r₂ : ℝ} (hm : m ≠ 0) (h₁ : r₁ ≠ 0)
(h₂ : r₂ ≠ 0) (hne : r₁ ^ 2 ≠ r₂ ^ 2)
(hr₁ : 2 * m * (E - m * ν ^ 2 * r₁ ^ 2 / 2) = ℓ ^ 2 / r₁ ^ 2)
(hr₂ : 2 * m * (E - m * ν ^ 2 * r₂ ^ 2 / 2) = ℓ ^ 2 / r₂ ^ 2) : ℓ ^ 2 = (m * ν * (r₁ * r₂)) ^ 2
Vieta's formula for the isotropic oscillator, sum of squared turning points. Formalized in Tau Ceti as TauCeti.isotropicOscillator_energy_eq.
TauCeti.isotropicOscillator_energy_eq {m ν ℓ E r₁ r₂ : ℝ} (hm : m ≠ 0) (h₁ : r₁ ≠ 0) (h₂ : r₂ ≠ 0)
(hne : r₁ ^ 2 ≠ r₂ ^ 2) (hr₁ : 2 * m * (E - m * ν ^ 2 * r₁ ^ 2 / 2) = ℓ ^ 2 / r₁ ^ 2)
(hr₂ : 2 * m * (E - m * ν ^ 2 * r₂ ^ 2 / 2) = ℓ ^ 2 / r₂ ^ 2) :
2 * E = m * ν ^ 2 * (r₁ ^ 2 + r₂ ^ 2)
Vieta's formula for the Kepler product of turning points. Formalized in Tau Ceti as TauCeti.kepler_sq_eq_neg_two_mul_mul_mul.
TauCeti.kepler_sq_eq_neg_two_mul_mul_mul {m κ ℓ E r₁ r₂ : ℝ} (hm : m ≠ 0) (h₁ : r₁ ≠ 0)
(h₂ : r₂ ≠ 0) (hne : r₁ ≠ r₂) (hr₁ : 2 * m * (E + κ / r₁) = ℓ ^ 2 / r₁ ^ 2)
(hr₂ : 2 * m * (E + κ / r₂) = ℓ ^ 2 / r₂ ^ 2) : ℓ ^ 2 = -2 * m * E * (r₁ * r₂)
Sources
Used by 1
TheoremWirtinger identity on manifolds#
For an invariant pair (form, J), the standard energy
density minus twice the symplectic area density is the Cauchy--Riemann defect square:
$\(e(F) - 2 \omega_x(F \partial_s, F \partial_t) =
\omega_x(F \partial_s + J_x F \partial_t, J_x(F \partial_s + J_x F \partial_t)).\)$
TauCeti.SmoothTwoForm.Invariant.stdComplexLineEnergyDensity_sub_two_mul_twoForm.{u_1, u_2, u_3}
{E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
[TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M]
[IsManifold I (↑⊤) M] {form : TauCeti.SmoothTwoForm I M}
{J : TauCeti.SmoothAlmostComplexStructure I M} (hinv : form.Invariant J) (x : M)
(F : ℝ × ℝ →ₗ[ℝ] TangentSpace I x) :
form.stdComplexLineEnergyDensity J x F -
2 *
TauCeti.SmoothBundleForm.eval₂ form x (F TauCeti.stdComplexLineReal)
(F TauCeti.stdComplexLineImag) =
TauCeti.SmoothBundleForm.eval₂ form x
(F TauCeti.stdComplexLineReal +
(fun x => ⇑(J.toEndomorphism x)) x (F TauCeti.stdComplexLineImag))
((fun x => ⇑(J.toEndomorphism x)) x
(F TauCeti.stdComplexLineReal +
(fun x => ⇑(J.toEndomorphism x)) x (F TauCeti.stdComplexLineImag)))
Lean
Formalized in Tau Ceti as TauCeti.SmoothTwoForm.Invariant.stdComplexLineEnergyDensity_sub_two_mul_twoForm.
Sources
TheoremWirtinger inequality#
For a compatible pair (ω, J) and any real-linear map out of the
standard complex line, twice the symplectic area density of the ordered coordinate pair is at
most the standard energy density: the local form of E(u) ≥ ∫ u^*ω.
TauCeti.SymplecticForm.two_mul_symplecticForm_le_stdComplexLineEnergyDensity.{u_1} {V : Type u_1}
[AddCommGroup V] [_root_.Module ℝ V] {J : TauCeti.AlmostComplexStructure V}
{ω : TauCeti.SymplecticForm V} (hcompat : ω.Compatible J) (F : ℝ × ℝ →ₗ[ℝ] V) :
2 *
(fun v w => (ω.toBilinForm v) w) (F TauCeti.stdComplexLineReal)
(F TauCeti.stdComplexLineImag) ≤
ω.stdComplexLineEnergyDensity J F
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.two_mul_symplecticForm_le_stdComplexLineEnergyDensity.
Other forms
The Wirtinger inequality. Formalized in Tau Ceti as TauCeti.SymplecticForm.Compatible.apply_le_wedgeNorm.
TauCeti.SymplecticForm.Compatible.apply_le_wedgeNorm.{u_1} {V : Type u_1} [AddCommGroup V]
[_root_.Module ℝ V] {ω : TauCeti.SymplecticForm V} {J : TauCeti.AlmostComplexStructure V}
(h : ω.Compatible J) (v w : V) : (fun v w => (ω.toBilinForm v) w) v w ≤ ω.wedgeNorm J v w
Wirtinger inequality on manifolds. Formalized in Tau Ceti as TauCeti.SmoothTwoForm.Compatible.two_mul_twoForm_le_stdComplexLineEnergyDensity.
TauCeti.SmoothTwoForm.Compatible.two_mul_twoForm_le_stdComplexLineEnergyDensity.{u_1, u_2, u_3}
{E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
[TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M]
[IsManifold I (↑⊤) M] {form : TauCeti.SmoothTwoForm I M}
{J : TauCeti.SmoothAlmostComplexStructure I M} (hcompat : form.Compatible J) (x : M)
(F : ℝ × ℝ →ₗ[ℝ] TangentSpace I x) :
2 *
TauCeti.SmoothBundleForm.eval₂ form x (F TauCeti.stdComplexLineReal)
(F TauCeti.stdComplexLineImag) ≤
form.stdComplexLineEnergyDensity J x F
Sources
Uses 1 · Used by 1
TheoremWitt's extension theorem#
Witt's extension theorem, for a linear isomorphism f : S ≃ₗ[ℝ] T between subspaces of two
symplectic vector spaces of the same finite dimension: if f preserves the restricted forms, it
is the restriction of a linear symplectomorphism.
TauCeti.SymplecticForm.exists_isSymplectomorphism_extend_linearEquiv.{u_1, u_2} {V : Type u_1}
{W : Type u_2} [AddCommGroup V] [_root_.Module ℝ V] [AddCommGroup W] [_root_.Module ℝ W]
[FiniteDimensional ℝ V] [FiniteDimensional ℝ W] (ω₁ : TauCeti.SymplecticForm V)
(ω₂ : TauCeti.SymplecticForm W) (hdim : Module.finrank ℝ V = Module.finrank ℝ W)
{S : Submodule ℝ V} {T : Submodule ℝ W} (f : ↥S ≃ₗ[ℝ] ↥T)
(hω :
∀ (x y : ↥S),
(fun v w => (ω₂.toBilinForm v) w) ↑(f x) ↑(f y) = (fun v w => (ω₁.toBilinForm v) w) ↑x ↑y) :
∃ e, ω₁.IsSymplectomorphism ω₂ e ∧ ∀ (x : ↥S), e ↑x = ↑(f x)
Lean
Formalized in Tau Ceti as TauCeti.SymplecticForm.exists_isSymplectomorphism_extend_linearEquiv.
Other forms
Witt's extension theorem for symplectic vector spaces. Formalized in Tau Ceti as TauCeti.SymplecticForm.exists_isSymplectomorphism_extend.
TauCeti.SymplecticForm.exists_isSymplectomorphism_extend.{u_1, u_2} {V : Type u_1} {W : Type u_2}
[AddCommGroup V] [_root_.Module ℝ V] [AddCommGroup W] [_root_.Module ℝ W] [FiniteDimensional ℝ V]
[FiniteDimensional ℝ W] (ω₁ : TauCeti.SymplecticForm V) (ω₂ : TauCeti.SymplecticForm W)
(hdim : Module.finrank ℝ V = Module.finrank ℝ W) {S : Submodule ℝ V} (f : ↥S →ₗ[ℝ] W)
(hf : Function.Injective ⇑f)
(hω :
∀ (x y : ↥S),
(fun v w => (ω₂.toBilinForm v) w) (f x) (f y) = (fun v w => (ω₁.toBilinForm v) w) ↑x ↑y) :
∃ e, ω₁.IsSymplectomorphism ω₂ e ∧ ∀ (x : ↥S), e ↑x = f x
Sources
Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.