PhyslibAlpha.ClassicalMechanics.CoupledSpringPotential

PhyslibAlpha
ClassicalMechanics
CoupledSpringPotential

Imports

/-
Copyright (c) 2026 Bjørn Kjos-Hanssen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bjørn Kjos-Hanssen
-/
module

public import Mathlib.Analysis.Calculus.Gradient.Basic
public import Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
public import Mathlib.LinearAlgebra.QuadraticForm.Basic
public import Mathlib.Analysis.Calculus.FDeriv.Analytic
public import Mathlib.Analysis.Analytic.IteratedFDeriv
public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
public import Mathlib.Analysis.InnerProductSpace.PiL2
public import PhyslibAlpha.Mathematics.PartialDerivativeTest

Coupled spring potential

As a proof of concept, we use the second derivative test in PhyslibAlpha.Mathematics.PartialDerivativeTest to prove that the coupled spring potential U := fun x : EuclideanSpace ℝ (Fin 2) => (x 0)^2 + x 0 * x 1 + (x 1)^2 has a local minimum at zero.

              @[expose] public section/-
The coupling potential is analytic everywhere (it is a polynomial).
-/
lemma couplingPotential_analyticAt (z : EuclideanSpace ℝ (Fin 2)) :
    AnalyticAt ℝ couplingPotential z := byz:EuclideanSpace ℝ (Fin 2)⊢ AnalyticAt ℝ couplingPotential z
  have h0 : AnalyticAt ℝ (fun x : EuclideanSpace ℝ (Fin 2) => x 0) z :=
    (EuclideanSpace.proj (𝕜 := ℝ) 0).analyticAt zz:EuclideanSpace ℝ (Fin 2)h0:AnalyticAt ℝ (fun x => x.ofLp 0) z⊢ AnalyticAt ℝ couplingPotential z
  have h1 : AnalyticAt ℝ (fun x : EuclideanSpace ℝ (Fin 2) => x 1) z :=
    (EuclideanSpace.proj (𝕜 := ℝ) 1).analyticAt zz:EuclideanSpace ℝ (Fin 2)h0:AnalyticAt ℝ (fun x => x.ofLp 0) zh1:AnalyticAt ℝ (fun x => x.ofLp 1) z⊢ AnalyticAt ℝ couplingPotential z
  unfold couplingPotentialz:EuclideanSpace ℝ (Fin 2)h0:AnalyticAt ℝ (fun x => x.ofLp 0) zh1:AnalyticAt ℝ (fun x => x.ofLp 1) z⊢ AnalyticAt ℝ (fun x => x.ofLp 0 ^ 2 + x.ofLp 0 * x.ofLp 1 + x.ofLp 1 ^ 2) z
  exact ((h0.pow 2).add (h0.mul h1)).add (h1.pow 2)All goals completed! 🐙

/-
The derivative of the coupling potential at any point, as an explicit
linear functional.
-/
lemma couplingPotential_hasFDerivAt (x : EuclideanSpace ℝ (Fin 2)) :
    HasFDerivAt couplingPotential
      ((2 * x 0 + x 1) • (EuclideanSpace.proj (𝕜 := ℝ) 0)
        + (x 0 + 2 * x 1) • (EuclideanSpace.proj (𝕜 := ℝ) 1)) x := byx:EuclideanSpace ℝ (Fin 2)⊢ HasFDerivAt couplingPotential
  ((2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1) x
  have h0 : HasFDerivAt (fun x : EuclideanSpace ℝ (Fin 2) => x 0)
    (EuclideanSpace.proj (𝕜 := ℝ) 0) x := by
    exact ContinuousLinearMap.hasFDerivAt (EuclideanSpace.proj (𝕜 := ℝ) 0)x:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) x⊢ HasFDerivAt couplingPotential
  ((2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1) xx:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) x⊢ HasFDerivAt couplingPotential
  ((2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1) x
  have h1 : HasFDerivAt (fun x : EuclideanSpace ℝ (Fin 2) => x 1)
    (EuclideanSpace.proj (𝕜 := ℝ) 1) x := by
    norm_num [hasFDerivAt_iff_isLittleO_nhds_zero]All goals completed! 🐙x:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) xh1:HasFDerivAt (fun x => x.ofLp 1) (EuclideanSpace.proj 1) x⊢ HasFDerivAt couplingPotential
  ((2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1) x;x:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) xh1:HasFDerivAt (fun x => x.ofLp 1) (EuclideanSpace.proj 1) x⊢ HasFDerivAt couplingPotential
  ((2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1) x
  convert! HasFDerivAt.add (HasFDerivAt.add (h0.pow 2) (h0.mul h1)) (h1.pow 2) using 1e'_12x:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) xh1:HasFDerivAt (fun x => x.ofLp 1) (EuclideanSpace.proj 1) xe_4✝:WithLp.instAddCommGroup 2 ((i : Fin 2) → (fun x => ℝ) i) = (PiLp.normedAddCommGroup 2 fun x => ℝ).toAddCommGrouphe✝¹:WithLp.instModule 2 ℝ ((i : Fin 2) → (fun x => ℝ) i) = (PiLp.normedSpace 2 ℝ fun x => ℝ).toModulee_6✝:(PiLp.topologicalSpace 2 fun x => ℝ) = PseudoMetricSpace.toUniformSpace.toTopologicalSpacee_8✝:Real.instAddCommGroup = Real.normedAddCommGroup.toAddCommGrouphe✝:Semiring.toModule = RCLike.toInnerProductSpaceReal.toModule⊢ (2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1 =
  (2 • x.ofLp 0 ^ (2 - 1)) • EuclideanSpace.proj 0 +
      (x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0) +
    (2 • x.ofLp 1 ^ (2 - 1)) • EuclideanSpace.proj 1
  exte'_12x:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) xh1:HasFDerivAt (fun x => x.ofLp 1) (EuclideanSpace.proj 1) xe_4✝:WithLp.instAddCommGroup 2 ((i : Fin 2) → (fun x => ℝ) i) = (PiLp.normedAddCommGroup 2 fun x => ℝ).toAddCommGrouphe✝¹:WithLp.instModule 2 ℝ ((i : Fin 2) → (fun x => ℝ) i) = (PiLp.normedSpace 2 ℝ fun x => ℝ).toModulee_6✝:(PiLp.topologicalSpace 2 fun x => ℝ) = PseudoMetricSpace.toUniformSpace.toTopologicalSpacee_8✝:Real.instAddCommGroup = Real.normedAddCommGroup.toAddCommGrouphe✝:Semiring.toModule = RCLike.toInnerProductSpaceReal.toModulex✝:EuclideanSpace ℝ (Fin 2)⊢ ((2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1) x✝ =
  ((2 • x.ofLp 0 ^ (2 - 1)) • EuclideanSpace.proj 0 +
        (x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0) +
      (2 • x.ofLp 1 ^ (2 - 1)) • EuclideanSpace.proj 1)
    x✝; norm_nume'_12x:EuclideanSpace ℝ (Fin 2)h0:HasFDerivAt (fun x => x.ofLp 0) (EuclideanSpace.proj 0) xh1:HasFDerivAt (fun x => x.ofLp 1) (EuclideanSpace.proj 1) xe_4✝:WithLp.instAddCommGroup 2 ((i : Fin 2) → (fun x => ℝ) i) = (PiLp.normedAddCommGroup 2 fun x => ℝ).toAddCommGrouphe✝¹:WithLp.instModule 2 ℝ ((i : Fin 2) → (fun x => ℝ) i) = (PiLp.normedSpace 2 ℝ fun x => ℝ).toModulee_6✝:(PiLp.topologicalSpace 2 fun x => ℝ) = PseudoMetricSpace.toUniformSpace.toTopologicalSpacee_8✝:Real.instAddCommGroup = Real.normedAddCommGroup.toAddCommGrouphe✝:Semiring.toModule = RCLike.toInnerProductSpaceReal.toModulex✝:EuclideanSpace ℝ (Fin 2)⊢ (2 * x.ofLp 0 + x.ofLp 1) * x✝.ofLp 0 + (x.ofLp 0 + 2 * x.ofLp 1) * x✝.ofLp 1 =
  2 * x.ofLp 0 * x✝.ofLp 0 + (x.ofLp 0 * x✝.ofLp 1 + x.ofLp 1 * x✝.ofLp 0) + 2 * x.ofLp 1 * x✝.ofLp 1; ringAll goals completed! 🐙/-
The gradient of the coupling potential vanishes at the origin.
-/
lemma couplingPotential_gradient_zero :
    gradient couplingPotential (!2[0, 0] : EuclideanSpace ℝ (Fin 2)) = 0 := by⊢ gradient couplingPotential !₂[0, 0] = 0
  convert! (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 2))).symm_apply_eq.mpr ?_convert_3⊢ fderiv ℝ couplingPotential !₂[0, 0] = (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 2))).toLinearEquiv 0;
  convert! HasFDerivAt.fderiv (couplingPotential_hasFDerivAt _) using 1e'_3⊢ (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin 2))).toLinearEquiv 0 =
  (2 * !₂[0, 0].ofLp 0 + !₂[0, 0].ofLp 1) • EuclideanSpace.proj 0 +
    (!₂[0, 0].ofLp 0 + 2 * !₂[0, 0].ofLp 1) • EuclideanSpace.proj 1
  norm_num [fderiv_apply_one_eq_deriv]All goals completed! 🐙

/-
The value of the second derivative quadratic map of the coupling potential.
-/
lemma couplingPotential_iteratedFDeriv_two (z : EuclideanSpace ℝ (Fin 2))
    (a b : EuclideanSpace ℝ (Fin 2)) :
    iteratedFDeriv ℝ 2 couplingPotential z ![a, b]
      = 2 * a 0 * b 0 + a 0 * b 1 + a 1 * b 0 + 2 * a 1 * b 1 := byz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1
  have h_second_deriv : fderiv ℝ (fderiv ℝ couplingPotential) z
    = (2 • (EuclideanSpace.proj (𝕜 := ℝ) 0).smulRight
    (EuclideanSpace.proj (𝕜 := ℝ) 0) + (EuclideanSpace.proj (𝕜 := ℝ) 0).smulRight
    (EuclideanSpace.proj (𝕜 := ℝ) 1) + (EuclideanSpace.proj (𝕜 := ℝ) 1).smulRight
    (EuclideanSpace.proj (𝕜 := ℝ) 0) + 2 • (EuclideanSpace.proj (𝕜 := ℝ) 1).smulRight
    (EuclideanSpace.proj (𝕜 := ℝ) 1)) := by
    refine' HasFDerivAt.fderiv _z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ HasFDerivAt (fderiv ℝ couplingPotential)
  (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
  zz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;
    rw [show fderiv ℝ couplingPotential = _ from funext fun x =>
      HasFDerivAt.fderiv (couplingPotential_hasFDerivAt x)z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ HasFDerivAt
  (fun x => (2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1)
  (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
  zz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ HasFDerivAt
  (fun x => (2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1)
  (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
  zz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ HasFDerivAt
  (fun x => (2 * x.ofLp 0 + x.ofLp 1) • EuclideanSpace.proj 0 + (x.ofLp 0 + 2 * x.ofLp 1) • EuclideanSpace.proj 1)
  (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
  zz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;
    rw [hasFDerivAt_iff_isLittleO_nhds_zeroz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ (fun h =>
    (2 * (z + h).ofLp 0 + (z + h).ofLp 1) • EuclideanSpace.proj 0 +
          ((z + h).ofLp 0 + 2 * (z + h).ofLp 1) • EuclideanSpace.proj 1 -
        ((2 * z.ofLp 0 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + 2 * z.ofLp 1) • EuclideanSpace.proj 1) -
      (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
              ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
            ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
          2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
        h) =o[nhds 0]
  fun h => hz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ (fun h =>
    (2 * (z + h).ofLp 0 + (z + h).ofLp 1) • EuclideanSpace.proj 0 +
          ((z + h).ofLp 0 + 2 * (z + h).ofLp 1) • EuclideanSpace.proj 1 -
        ((2 * z.ofLp 0 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + 2 * z.ofLp 1) • EuclideanSpace.proj 1) -
      (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
              ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
            ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
          2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
        h) =o[nhds 0]
  fun h => hz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ (fun h =>
    (2 * (z + h).ofLp 0 + (z + h).ofLp 1) • EuclideanSpace.proj 0 +
          ((z + h).ofLp 0 + 2 * (z + h).ofLp 1) • EuclideanSpace.proj 1 -
        ((2 * z.ofLp 0 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + 2 * z.ofLp 1) • EuclideanSpace.proj 1) -
      (2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
              ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
            ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
          2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1))
        h) =o[nhds 0]
  fun h => hz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;
    norm_num [Asymptotics.isLittleO_iff]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)⊢ ∀ ⦃c : ℝ⦄,
  0 < c →
    ∀ᶠ (x : EuclideanSpace ℝ (Fin 2)) in nhds 0,
      ‖(2 * (z.ofLp 0 + x.ofLp 0) + (z.ofLp 1 + x.ofLp 1)) • EuclideanSpace.proj 0 +
                (z.ofLp 0 + x.ofLp 0 + 2 * (z.ofLp 1 + x.ofLp 1)) • EuclideanSpace.proj 1 -
              ((2 * z.ofLp 0 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + 2 * z.ofLp 1) • EuclideanSpace.proj 1) -
            (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0 • EuclideanSpace.proj 1 +
                x.ofLp 1 • EuclideanSpace.proj 0 +
              2 • x.ofLp 1 • EuclideanSpace.proj 1)‖ ≤
        c * ‖x‖z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;
    intro ε hεz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < ε⊢ ∀ᶠ (x : EuclideanSpace ℝ (Fin 2)) in nhds 0,
  ‖(2 * (z.ofLp 0 + x.ofLp 0) + (z.ofLp 1 + x.ofLp 1)) • EuclideanSpace.proj 0 +
            (z.ofLp 0 + x.ofLp 0 + 2 * (z.ofLp 1 + x.ofLp 1)) • EuclideanSpace.proj 1 -
          ((2 * z.ofLp 0 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + 2 * z.ofLp 1) • EuclideanSpace.proj 1) -
        (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0 +
          2 • x.ofLp 1 • EuclideanSpace.proj 1)‖ ≤
    ε * ‖x‖z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; filter_upwards [Metric.ball_mem_nhds _ hε] with x hxz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 ε⊢ ‖(2 * (z.ofLp 0 + x.ofLp 0) + (z.ofLp 1 + x.ofLp 1)) • EuclideanSpace.proj 0 +
          (z.ofLp 0 + x.ofLp 0 + 2 * (z.ofLp 1 + x.ofLp 1)) • EuclideanSpace.proj 1 -
        ((2 * z.ofLp 0 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + 2 * z.ofLp 1) • EuclideanSpace.proj 1) -
      (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0 +
        2 • x.ofLp 1 • EuclideanSpace.proj 1)‖ ≤
  ε * ‖x‖z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; ring_nfz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 ε⊢ ‖(z.ofLp 0 * 2 + x.ofLp 0 * 2 + z.ofLp 1 + x.ofLp 1) • EuclideanSpace.proj 0 +
          (z.ofLp 0 + x.ofLp 0 + z.ofLp 1 * 2 + x.ofLp 1 * 2) • EuclideanSpace.proj 1 -
        ((z.ofLp 0 * 2 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + z.ofLp 1 * 2) • EuclideanSpace.proj 1) -
      (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0 +
        2 • x.ofLp 1 • EuclideanSpace.proj 1)‖ ≤
  ε * ‖x‖z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;
    erw [show ((z.ofLp 0 * 2 + x.ofLp 0 * 2 + z.ofLp 1 + x.ofLp 1) • EuclideanSpace.proj 0
      + (z.ofLp 0 + x.ofLp 0 + z.ofLp 1 * 2 + x.ofLp 1 * 2) • EuclideanSpace.proj 1
      - ((z.ofLp 0 * 2 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + z.ofLp 1 * 2)
      • EuclideanSpace.proj 1) - (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0
      • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0 + 2 • x.ofLp 1
      • EuclideanSpace.proj 1) : EuclideanSpace ℝ (Fin 2) →L[ℝ] ℝ) = 0 from byz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 ε⊢ (z.ofLp 0 * 2 + x.ofLp 0 * 2 + z.ofLp 1 + x.ofLp 1) • EuclideanSpace.proj 0 +
        (z.ofLp 0 + x.ofLp 0 + z.ofLp 1 * 2 + x.ofLp 1 * 2) • EuclideanSpace.proj 1 -
      ((z.ofLp 0 * 2 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + z.ofLp 1 * 2) • EuclideanSpace.proj 1) -
    (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0 +
      2 • x.ofLp 1 • EuclideanSpace.proj 1) =
  0z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1
        extz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 εx✝:EuclideanSpace ℝ (Fin 2)⊢ ((z.ofLp 0 * 2 + x.ofLp 0 * 2 + z.ofLp 1 + x.ofLp 1) • EuclideanSpace.proj 0 +
          (z.ofLp 0 + x.ofLp 0 + z.ofLp 1 * 2 + x.ofLp 1 * 2) • EuclideanSpace.proj 1 -
        ((z.ofLp 0 * 2 + z.ofLp 1) • EuclideanSpace.proj 0 + (z.ofLp 0 + z.ofLp 1 * 2) • EuclideanSpace.proj 1) -
      (2 • x.ofLp 0 • EuclideanSpace.proj 0 + x.ofLp 0 • EuclideanSpace.proj 1 + x.ofLp 1 • EuclideanSpace.proj 0 +
        2 • x.ofLp 1 • EuclideanSpace.proj 1))
    x✝ =
  0 x✝z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; norm_numz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 εx✝:EuclideanSpace ℝ (Fin 2)⊢ (z.ofLp 0 * 2 + x.ofLp 0 * 2 + z.ofLp 1 + x.ofLp 1) * x✝.ofLp 0 +
        (z.ofLp 0 + x.ofLp 0 + z.ofLp 1 * 2 + x.ofLp 1 * 2) * x✝.ofLp 1 -
      ((z.ofLp 0 * 2 + z.ofLp 1) * x✝.ofLp 0 + (z.ofLp 0 + z.ofLp 1 * 2) * x✝.ofLp 1) -
    (2 * (x.ofLp 0 * x✝.ofLp 0) + x.ofLp 0 * x✝.ofLp 1 + x.ofLp 1 * x✝.ofLp 0 + 2 * (x.ofLp 1 * x✝.ofLp 1)) =
  0z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; ringAll goals completed! 🐙z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 ε⊢ ‖0‖ ≤ ε * ‖x‖z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; norm_num [hε.le]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)ε:ℝhε:0 < εx:EuclideanSpace ℝ (Fin 2)hx:x ∈ Metric.ball 0 ε⊢ 0 ≤ ε * ‖x‖z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;
    positivityAll goals completed! 🐙z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1;z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ (iteratedFDeriv ℝ 2 couplingPotential z) ![a, b] =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1
  rw [iteratedFDeriv_succ_apply_rightz:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ ((iteratedFDeriv ℝ 1 (fun y => fderiv ℝ couplingPotential y) z) (Fin.init ![a, b])) (![a, b] (Fin.last 1)) =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ ((iteratedFDeriv ℝ 1 (fun y => fderiv ℝ couplingPotential y) z) (Fin.init ![a, b])) (![a, b] (Fin.last 1)) =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ ((iteratedFDeriv ℝ 1 (fun y => fderiv ℝ couplingPotential y) z) (Fin.init ![a, b])) (![a, b] (Fin.last 1)) =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; simp +decide [h_second_deriv]z:EuclideanSpace ℝ (Fin 2)a:EuclideanSpace ℝ (Fin 2)b:EuclideanSpace ℝ (Fin 2)h_second_deriv:fderiv ℝ (fderiv ℝ couplingPotential) z =
  2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 0) +
        ContinuousLinearMap.smulRight (EuclideanSpace.proj 0) (EuclideanSpace.proj 1) +
      ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 0) +
    2 • ContinuousLinearMap.smulRight (EuclideanSpace.proj 1) (EuclideanSpace.proj 1)⊢ 2 * ((Fin.init ![a, b] 0).ofLp 0 * b.ofLp 0) + (Fin.init ![a, b] 0).ofLp 0 * b.ofLp 1 +
      (Fin.init ![a, b] 0).ofLp 1 * b.ofLp 0 +
    2 * ((Fin.init ![a, b] 0).ofLp 1 * b.ofLp 1) =
  2 * a.ofLp 0 * b.ofLp 0 + a.ofLp 0 * b.ofLp 1 + a.ofLp 1 * b.ofLp 0 + 2 * a.ofLp 1 * b.ofLp 1; ring!All goals completed! 🐙;/-
The second derivative quadratic map of the coupling potential is positive definite
at the origin.
-/
lemma couplingPotential_posDef :
    (iteratedFDerivQuadraticMap couplingPotential
    (!2[0, 0] : EuclideanSpace ℝ (Fin 2))).PosDef := by⊢ (iteratedFDerivQuadraticMap couplingPotential !₂[0, 0]).PosDef
  intros y hyy:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0⊢ 0 < (iteratedFDerivQuadraticMap couplingPotential !₂[0, 0]) y;
  convert! (show 0 < 2 * y 0 ^ 2 + 2 * y 0 * y 1 + 2 * y 1 ^ 2 by⊢ (iteratedFDerivQuadraticMap couplingPotential !₂[0, 0]).PosDef
              exact not_le.mp fun h => hy <| byy:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y = 0
                ext iy:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0i:Fin 2⊢ y.ofLp i = WithLp.ofLp 0 i
                fin_cases i«0»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp ((fun i => i) ⟨0, ⋯⟩) = WithLp.ofLp 0 ((fun i => i) ⟨0, ⋯⟩)«1»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp ((fun i => i) ⟨1, ⋯⟩) = WithLp.ofLp 0 ((fun i => i) ⟨1, ⋯⟩) <;>«0»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp ((fun i => i) ⟨0, ⋯⟩) = WithLp.ofLp 0 ((fun i => i) ⟨0, ⋯⟩)«1»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp ((fun i => i) ⟨1, ⋯⟩) = WithLp.ofLp 0 ((fun i => i) ⟨1, ⋯⟩) norm_num«1»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp 1 = 0 <;>«0»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp 0 = 0«1»y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0h:2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 ≤ 0⊢ y.ofLp 1 = 0 nlinarith! [sq_nonneg (y.ofLp 0 + y.ofLp 1)]All goals completed! 🐙) using 1
  generalize_proofs at *e'_4y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0pf✝¹:Nat.AtLeastTwo 2pf✝:NeZero 2⊢ (iteratedFDerivQuadraticMap couplingPotential !₂[0, 0]) y =
  2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2;
  convert! couplingPotential_iteratedFDeriv_two !2[0, 0] y y using 1e'_3y:EuclideanSpace ℝ (Fin 2)hy:y ≠ 0pf✝¹:Nat.AtLeastTwo 2pf✝:NeZero 2⊢ 2 * y.ofLp 0 ^ 2 + 2 * y.ofLp 0 * y.ofLp 1 + 2 * y.ofLp 1 ^ 2 =
  2 * y.ofLp 0 * y.ofLp 0 + y.ofLp 0 * y.ofLp 1 + y.ofLp 1 * y.ofLp 0 + 2 * y.ofLp 1 * y.ofLp 1; ring!All goals completed! 🐙lemma coupled_spring_potential :
    let U := fun x : EuclideanSpace ℝ (Fin 2) => (x 0)^2 + x 0 * x 1 + (x 1)^2
    IsLocalMin U {
        ofLp := ![0,0]
    } := by⊢ let U := fun x => x.ofLp 0 ^ 2 + x.ofLp 0 * x.ofLp 1 + x.ofLp 1 ^ 2;
IsLocalMin U !₂[0, 0]
  show IsLocalMin couplingPotential (!2[0, 0] : EuclideanSpace ℝ (Fin 2))⊢ IsLocalMin couplingPotential !₂[0, 0]
  exact second_derivative_test_analyticAt couplingPotential_gradient_zero
    (couplingPotential_analyticAt _) couplingPotential_posDefAll goals completed! 🐙