theorem A.443 Sturm separation theorem

Rests on

• depends_on lemma A.442 The Wronskian of the accessory equation is constant ¶
  • depends_on lemma A.439 Existence, uniqueness, and the structure of the zeros ¶
    • depends_on corollary 9.9 Linear equations: existence on the whole interval ¶
      • depends_on definition 9.2 Linear equation; homogeneity ¶
        • depends_on definition 9.1 Ordinary differential equation ¶
      • depends_on remark 9.3 Normal form and first-order systems ¶
      • depends_on theorem 9.8 Picard–Lindelöf ¶
        • depends_on definition 9.4 Lipschitz condition ¶
        • depends_on equation 9.3 eq:slt-ode-system ¶
        • depends_on lemma 9.6 Weierstrass $M$-test; uniform limits are continuous ¶
        • proves proof ch:07-odes-sturm-liouville@proof-2 ¶
      • proves proof ch:07-odes-sturm-liouville@proof-3 ¶
    • depends_on definition A.438 Momentum variable and the accessory system ¶
      • depends_on equation 16.49 eq:calcvar-jacobi ¶
      • depends_on equation 9.3 eq:slt-ode-system ¶ ↺
    • proves proof app:A-long-proofs@proof-261 ¶
  • depends_on lemma 9.56 Lagrange identity ¶
    • depends_on definition 9.54 Sturm–Liouville differential operator ¶
    • proves proof ch:07-odes-sturm-liouville@proof-28 ¶
  • proves proof app:A-long-proofs@proof-264 ¶
• depends_on theorem 7.23 Intermediate value theorem ¶
  • depends_on axiom 7.1 Completeness of $\R$ ¶
  • depends_on definition 7.20 Continuity at a point ¶
    • depends_on definition 7.16 Limit ¶
      • depends_on definition 7.2 Absolute value ¶
      • depends_on definition 7.9 Real function ¶
        • depends_on definition 3.43 Map ¶
    • depends_on equation 7.7 eq:ana-limit-left ¶
    • depends_on equation 7.5 eq:ana-limit-right ¶
  • proves proof ch:05-real-analysis@proof-8 ¶
• proves proof app:A-long-proofs@proof-265 ¶

Supports

Nothing declares a dependency on this node yet.