Documentation

LeanPool.PoincareThreeBody.DifferentialDependence

Coordinate minors and functional dependence #

Two phase covectors are dependent exactly when all of their two-by-two coordinate minors vanish. This file proves the direction needed for nonintegrability. It converts the scalar analytic identities naturally produced by coefficient induction into failure of the challenge's LinearIndependent predicate.

source
def LeanPool.PoincareThreeBody.phaseCovectorMinor (first second : PhaseSpace →L[ℝ] ℝ) (i j : Fin 4) :
ℝ

A two-by-two coordinate minor of a pair of phase covectors.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LeanPool.PoincareThreeBody.phaseCovectorMinor_comp_self_eq_zero {observable : PhaseSpace → ℝ} {scalarFunction : ℝ → ℝ} {state : PhaseSpace} (hobservable : DifferentiableAt ℝ observable state) (hscalar : DifferentiableAt ℝ scalarFunction (observable state)) (i j : Fin 4) :
    phaseCovectorMinor (fderiv ℝ observable state) (fderiv ℝ (fun (candidate : PhaseSpace) => scalarFunction (observable candidate)) state) i j = 0

    A differentiable scalar function of an observable has zero coordinate minors with that observable.

    source
    theorem LeanPool.PoincareThreeBody.phaseCovector_eq_zero_of_coordinates_eq_zero {covector : PhaseSpace →L[ℝ] ℝ} (hzero : ∀ (i : Fin 4), covector (coordinateVector i) = 0) :
    covector = 0

    A phase covector vanishing on all four coordinate vectors is zero.

    source
    theorem LeanPool.PoincareThreeBody.not_linearIndependent_pair_of_eq_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] {first second : V} {scalar : ℝ} (hsecond : second = scalar • first) :
    ¬LinearIndependent ℝ ![first, second]

    A pair consisting of a vector and one of its scalar multiples is not linearly independent.

    source
    theorem LeanPool.PoincareThreeBody.not_linearIndependent_phaseCovectors_of_minors_eq_zero {first second : PhaseSpace →L[ℝ] ℝ} (hminor : ∀ (i j : Fin 4), phaseCovectorMinor first second i j = 0) :
    ¬LinearIndependent ℝ ![first, second]

    If every coordinate minor vanishes, two concrete phase covectors are dependent.

    source
    theorem LeanPool.PoincareThreeBody.linearIndependent_phaseCovectors_of_minor_ne_zero {first second : PhaseSpace →L[ℝ] ℝ} {i j : Fin 4} (hminor : phaseCovectorMinor first second i j ≠ 0) :
    LinearIndependent ℝ ![first, second]

    One nonzero coordinate minor certifies linear independence of a pair of covectors.

    source
    theorem LeanPool.PoincareThreeBody.phaseCovectorMinor_eq_zero_of_not_linearIndependent {first second : PhaseSpace →L[ℝ] ℝ} (hdependent : ¬LinearIndependent ℝ ![first, second]) (i j : Fin 4) :
    phaseCovectorMinor first second i j = 0

    For a pair of concrete phase covectors, dependence is equivalent to vanishing of all coordinate minors.

    source
    theorem LeanPool.PoincareThreeBody.not_linearIndependent_fderiv_of_minors_eq_zero {first second : PhaseSpace → ℝ} {state : PhaseSpace} (hminor : ∀ (i j : Fin 4), phaseCovectorMinor (fderiv ℝ first state) (fderiv ℝ second state) i j = 0) :
    ¬LinearIndependent ℝ ![fderiv ℝ first state, fderiv ℝ second state]

    Coordinate-minor formulation for differentials of two observables.