OAI/Analysis/CoulombTransport/CoulombSupportExistence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.CoulombSupportExistence.stationary_eq line 17

   Source documentation

   The two explicit conventions for the stationary field coincide.

   theorem stationary_eq (a : E3) :
       StationaryMap.stationary a = stationaryEquation 20 a := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.StationaryMap.stationary

2. def OAI.Problem356.CoulombSupportExistence.D line 28
3. def OAI.Problem356.CoulombSupportExistence.H line 31
4. theorem OAI.Problem356.CoulombSupportExistence.D_eq line 37
5. theorem OAI.Problem356.CoulombSupportExistence.nonempty_coulombLocalSupportingCharts line 45

   Source documentation

   The actual Coulomb stationary charts admit a local supporting potential with exact equality precisely on the stationary branch.

   theorem nonempty_coulombLocalSupportingCharts (k : Fin 3) :
       Nonempty (LocalSupportingCharts
         (StationaryMap.jointPotential (axisVector k))
         (stationaryEquation 20 (axisVector k))
         (axisVector k) (0, -axisVector k)) := by
   …

   Mentions: OAI.Problem356.StationaryMap.jointPotential

6. theorem OAI.Problem356.CoulombSupportExistence.nonempty_coulombLocalSupportingCharts_stationary line 102

   Source documentation

   The supporting charts in the scalar-potential stationary convention.

   theorem nonempty_coulombLocalSupportingCharts_stationary (k : Fin 3) :
       Nonempty (LocalSupportingCharts
         (StationaryMap.jointPotential (axisVector k))
         (StationaryMap.stationary (axisVector k))
         (axisVector k) (0, -axisVector k)) := by
   …

   Mentions: OAI.Problem356.StationaryMap.jointPotential, OAI.Problem356.StationaryMap.stationary