OAI/Analysis/CoulombTransport/CoulombBranches.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.CoulombBranches.stationary_charts_of_center_derivatives line 17

   Source documentation

   The concrete K=20 matrix certificate discharges every invertibility premise of the local branch theorem once the two partial derivatives are identified.

   theorem stationary_charts_of_center_derivatives
       (G : E3 × (E3 × E3) → E3 × E3) (k : Fin 3) (p : E3) (s : E3 × E3)
       (hG : ContDiffAt ℝ ω G (p, s)) (hzero : G (p, s) = 0)
       (hstate : fderiv ℝ G (p, s) ∘L ContinuousLinearMap.inr ℝ E3 (E3 × E3) =
         stateOperator k)
       (hparameter : fderiv ℝ G (p, s) ∘L ContinuousLinearMap.inl ℝ E3 (E3 × E3) =
         parameterOperator k) :
       Nonempty (AnalyticStationaryCharts G p s) := by
   …

   Mentions: OAI.Problem356.E3