OAI/Geometry/RCD/Sobolev/RadialEnergyUnits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.radialEnergyConstant line 10
2. theorem OAI.RegularPointCoordinates.radialEnergyConstant_pos line 16
3. theorem OAI.RegularPointCoordinates.radial_energy_natural_units line 25

   Source documentation

   The testing radius s/64 and its Poincare constant cancel all length units in the weak-radial interior estimate.

   theorem radial_energy_natural_units {K G ε A B J Cχ s κ σ V L I b t : ℝ} {n : ℕ}
       (hs : 0 < s) (hs1 : s ≤ 1) (hκ : 0 ≤ κ) (hσ : 0 ≤ σ) (hV : 0 ≤ V)
       (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A) (hε : 0 ≤ ε) (hCχ : 0 ≤ Cχ) (hI : 0 ≤ I)
       (hL : L = ((n + 2 : ℕ) : ℝ) * max (1 + ε) (A * s))
       (ht : t ≤ 8 * (L ^ 2 * b ^ 2 * (4096 * Cχ * (J + B / 2) * σ + κ * A ^ 2 * s ^ 2 * V)) +
         4 * (G / (s / 64)) ^ 2 *
           (2 * I + 2 * (((n : ℝ) * (1 + ε)) ^ 2 * b ^ 2) * (σ * (B * s ^ 2)) +
             4 * (annularPoincareConstant K n * (s / 64) ^ 2) *
               (L ^ 2 * b ^ 2 * (4096 * Cχ * (J + B / 2) * σ + κ * A ^ 2 * s ^ 2 * V)))) :
       t ≤ radialEnergyConstant K n G ε A B J Cχ *
         (I / (s / 64) ^ 2 + (σ + κ * s ^ 2 * V) * b ^ 2) := by
   …

   Mentions: OAI.RegularPointCoordinates.annularPoincareConstant, OAI.RegularPointCoordinates.radialEnergyConstant