OAI/Analysis/CoulombTransport/CoulombSupportSeparated.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.CoulombSupportExistence.outside_central_ball line 13
2. theorem OAI.Problem356.CoulombSupportExistence.exists_separated_shrink line 25

   Source documentation

   Shrink both local domains before forming the global contact predicate. Every parameter of the entire retained graph, not just parameters in a later component ball, has both outer coordinates outside the fixed central ball.

   theorem exists_separated_shrink {a : E3} (ha : ‖a‖ = 1)
       (C : LocalSupportingCharts (jointPotential a) (stationary a) a (0, -a)) :
       ∃ D : LocalSupportingCharts (jointPotential a) (stationary a) a (0, -a),
         ∀ y ∈ D.charts.central.source,
           y ∉ ball (0 : E3) (1 / 4 : ℝ) ∧
             D.charts.opposite y ∉ ball (0 : E3) (1 / 4 : ℝ) := by
   …

   Mentions: OAI.Problem356.E3, OAI.Problem356.CoulombSupportExistence.D

3. theorem OAI.Problem356.CoulombSupportExistence.exists_coulombLocalSupportingCharts_separated line 44

   Source documentation

   Unconditional actual Coulomb supporting charts with graph-wide exclusion of both outer coordinates from a common fixed central neighborhood.

   theorem exists_coulombLocalSupportingCharts_separated (k : Fin 3) :
       ∃ C : LocalSupportingCharts (jointPotential (axisVector k))
         (stationary (axisVector k)) (axisVector k) (0, -axisVector k),
         ∀ y ∈ C.charts.central.source,
           y ∉ ball (0 : E3) (1 / 4 : ℝ) ∧
             C.charts.opposite y ∉ ball (0 : E3) (1 / 4 : ℝ) := by
   …

   Mentions: OAI.Problem356.E3