OAI/Analysis/CoulombTransport/CoulombCoercivity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem356.CoulombCalculus.pairHessian_quadratic_lower_of_two_thirds line 16

   Source documentation

   A uniform lower Hessian bound away from a Coulomb collision.

   theorem pairHessian_quadratic_lower_of_two_thirds {a : E}
       (ha : (2 : ℝ) / 3 ≤ ‖a‖) (u : E) :
       -(27 / 8 : ℝ) * ‖u‖ ^ 2 ≤ ⟪u, pairHessian a u⟫ := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.pairHessian

2. theorem OAI.Problem356.CoulombCalculus.regularized_hessian_coercive_of_separated line 33

   Source documentation

   The explicit K=20 regularization dominates every negative Coulomb Hessian contribution on a domain where all three pair distances are at least 2/3.

   theorem regularized_hessian_coercive_of_separated
       {a b c : E} (ha : (2 : ℝ) / 3 ≤ ‖a‖)
       (hb : (2 : ℝ) / 3 ≤ ‖b‖) (hc : (2 : ℝ) / 3 ≤ ‖c‖) (u v : E) :
       (79 / 8 : ℝ) * (‖u‖ ^ 2 + ‖v‖ ^ 2) ≤
         20 * (‖u‖ ^ 2 + ‖v‖ ^ 2) +
           ⟪u, pairHessian a u⟫ +
           ⟪u - v, pairHessian b (u - v)⟫ +
           ⟪v, pairHessian c v⟫ := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.pairHessian

3. theorem OAI.Problem356.CoulombCalculus.regularized_hessian_pos_of_separated line 50

   Source documentation

   Strict positivity for every nonzero state direction.

   theorem regularized_hessian_pos_of_separated
       {a b c : E} (ha : (2 : ℝ) / 3 ≤ ‖a‖)
       (hb : (2 : ℝ) / 3 ≤ ‖b‖) (hc : (2 : ℝ) / 3 ≤ ‖c‖)
       {u v : E} (huv : u ≠ 0 ∨ v ≠ 0) :
       0 < 20 * (‖u‖ ^ 2 + ‖v‖ ^ 2) +
           ⟪u, pairHessian a u⟫ +
           ⟪u - v, pairHessian b (u - v)⟫ +
           ⟪v, pairHessian c v⟫ := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.pairHessian

4. def OAI.Problem356.CoulombCalculus.regularizedStateHessian line 67

   Source documentation

   The regularized state-Jacobian, written in component form suitable for the parameter/state stationarity equation.

   def regularizedStateHessian (a b c : E) : (E × E) →L[ℝ] E × E :=
   …

5. theorem OAI.Problem356.CoulombCalculus.regularizedStateHessian_apply line 77
6. theorem OAI.Problem356.CoulombCalculus.regularizedStateHessian_quadratic line 83

   Source documentation

   Expansion of the product-state quadratic form.

   theorem regularizedStateHessian_quadratic (a b c : E) (q : E × E) :
       ⟪q.1, (regularizedStateHessian a b c q).1⟫ +
           ⟪q.2, (regularizedStateHessian a b c q).2⟫ =
         20 * (‖q.1‖ ^ 2 + ‖q.2‖ ^ 2) +
           ⟪q.1, pairHessian a q.1⟫ +
           ⟪q.1 - q.2, pairHessian b (q.1 - q.2)⟫ +
           ⟪q.2, pairHessian c q.2⟫ := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.regularizedStateHessian, OAI.Problem356.CoulombCalculus.pairHessian

7. theorem OAI.Problem356.CoulombCalculus.regularizedStateHessian_coercive line 96

   Source documentation

   Quantitative coercivity of the state-Jacobian in the actual max product norm.

   theorem regularizedStateHessian_coercive
       {a b c : E} (ha : (2 : ℝ) / 3 ≤ ‖a‖)
       (hb : (2 : ℝ) / 3 ≤ ‖b‖) (hc : (2 : ℝ) / 3 ≤ ‖c‖) (q : E × E) :
       (79 / 8 : ℝ) * ‖q‖ ^ 2 ≤
         ⟪q.1, (regularizedStateHessian a b c q).1⟫ +
           ⟪q.2, (regularizedStateHessian a b c q).2⟫ := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.regularizedStateHessian

8. theorem OAI.Problem356.CoulombCalculus.regularizedStateHessian_pos line 114

   Source documentation

   Strict positivity in every nonzero direction.

   theorem regularizedStateHessian_pos
       {a b c : E} (ha : (2 : ℝ) / 3 ≤ ‖a‖)
       (hb : (2 : ℝ) / 3 ≤ ‖b‖) (hc : (2 : ℝ) / 3 ≤ ‖c‖)
       {q : E × E} (hq : q ≠ 0) :
       0 < ⟪q.1, (regularizedStateHessian a b c q).1⟫ +
           ⟪q.2, (regularizedStateHessian a b c q).2⟫ :=
   …

   Mentions: OAI.Problem356.CoulombCalculus.regularizedStateHessian

9. theorem OAI.Problem356.CoulombCalculus.hasFDerivAt_regularizedStateGradient line 126

   Source documentation

   The explicit Jacobian of the regularized Coulomb stationarity equation. The constant vector in the second component accommodates the chosen outer potential and has no effect on the Hessian.

   theorem hasFDerivAt_regularizedStateGradient (y k : E) {s : E × E}
       (hxy : s.1 - y ≠ 0) (hxz : s.1 - s.2 ≠ 0) (hzy : s.2 - y ≠ 0) :
       HasFDerivAt
         (fun p : E × E =>
           (pairGradient (p.1 - y) + pairGradient (p.1 - p.2) + (20 : ℝ) • p.1,
             -pairGradient (p.1 - p.2) + pairGradient (p.2 - y) +
               (20 : ℝ) • p.2 + k))
         (regularizedStateHessian (s.1 - y) (s.1 - s.2) (s.2 - y)) s := by
   …

   Mentions: OAI.Problem356.CoulombCalculus.pairGradient, OAI.Problem356.CoulombCalculus.regularizedStateHessian