OAI/Geometry/SurfaceImmersion/Correction/CorrectionScaleAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.ExactCorrection.scale_quotient_product line 11
2. lemma OAI.ClosedSurfaceR4.ExactCorrection.scale_ratio_power line 15
3. lemma OAI.ClosedSurfaceR4.ExactCorrection.scale_ratio_power_linear line 24
4. lemma OAI.ClosedSurfaceR4.ExactCorrection.scale_cubic_quotient line 29
5. theorem OAI.ClosedSurfaceR4.ExactCorrection.error_exponents_ge_common line 40

   Source documentation

   The six exponents remain above the common exponent used in the all-order recurrence, including the smaller next-block amplitude.

   theorem error_exponents_ge_common {k : ℝ} (hk : 10 ≤ k) :
       (1 / 5 : ℝ) ≤ (13 * k + 8) / 5 ∧
       (1 / 5 : ℝ) ≤ (3 * k - 18) / 5 ∧
       (1 / 5 : ℝ) ≤ (18 * k + 8) / 5 ∧
       (1 / 5 : ℝ) ≤ (38 * k + 28) / 5 ∧
       (1 / 5 : ℝ) ≤ (13 * k + 8) / 5 ∧
       (1 / 5 : ℝ) ≤ (33 * k + 28) / 5 := by
   …

6. theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_mode_scale line 54

   Source documentation

   Exact normalization of the small-mode error term.

   theorem normalized_mode_scale {t : ℝ} (ht : 0 < t) (k : ℝ) :
       (t ^ k * (t ^ (6 / 5 : ℝ) / t ^ (11 / 10 : ℝ)) ^ (40 * (k + 1))) /
         (t ^ ((6 / 5 : ℝ) * (k + 1))) ^ (2 : ℕ) = t ^ ((13 * k + 8) / 5) := by
   …

7. theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_cubic_scale line 62

   Source documentation

   Exact normalization of the cubic error term.

   theorem normalized_cubic_scale {t : ℝ} (ht : 0 < t) (k : ℝ) :
       ((t ^ k) ^ (3 : ℕ) / t ^ (6 / 5 : ℝ)) /
         (t ^ ((6 / 5 : ℝ) * (k + 1))) ^ (2 : ℕ) = t ^ ((3 * k - 18) / 5) := by
   …

8. theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_defect_tail_scales line 70

   Source documentation

   The two powers in the smoothing defect, before their coefficients.

   theorem normalized_defect_tail_scales {t : ℝ} (ht : 0 < t) (k : ℝ) :
       ((t ^ k) ^ (2 : ℕ) * (t ^ (11 / 10 : ℝ) / t) ^ (40 * (k + 1))) /
           (t ^ ((6 / 5 : ℝ) * (k + 1))) ^ (2 : ℕ) = t ^ ((18 * k + 8) / 5) ∧
       ((t ^ k) ^ (2 : ℕ) * (t ^ (6 / 5 : ℝ) / t) ^ (40 * (k + 1))) /
           (t ^ ((6 / 5 : ℝ) * (k + 1))) ^ (2 : ℕ) = t ^ ((38 * k + 28) / 5) := by
   …

9. theorem OAI.ClosedSurfaceR4.ExactCorrection.normalized_cross_tail_scales line 85

   Source documentation

   The two powers in the bilinear cross term, before their coefficients.

   theorem normalized_cross_tail_scales {t : ℝ} (ht : 0 < t) (k : ℝ) :
       (t ^ k * (t ^ (11 / 10 : ℝ) / t) ^ (40 * (k + 1))) /
           (t ^ ((6 / 5 : ℝ) * (k + 1))) ^ (2 : ℕ) = t ^ ((13 * k + 8) / 5) ∧
       (t ^ k * (t ^ (6 / 5 : ℝ) / t) ^ (40 * (k + 1))) /
           (t ^ ((6 / 5 : ℝ) * (k + 1))) ^ (2 : ℕ) = t ^ ((33 * k + 28) / 5) := by
   …