GoodMomentConstant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Absorb the proved good-word costs into one absolute square-root mass constant.

lemma OAI.TwoPointCorrelations.positive_nat_power_exp line 11

theorem OAI.TwoPointCorrelations.eventually_good_moment_constant line 17

Source documentation

The threshold may depend on the fixed harmonic mass. The base constant is absolute; the mass keeps its square-root exponent.

theorem eventually_good_moment_constant (W : ℝ) (hW : 1 ≤ W) :
    ∀ᶠ L : ℝ in atTop, ∀ J k S : ℕ,
      1 ≤ J → L / 2 ≤ (k : ℝ) → (S : ℝ) ≤ L ^ (1 / 4 : ℝ) →
      Real.exp (108 * L) * (2 : ℝ) ^ (4 * k * J + 2 * S) *
        Real.exp (64 * k * J) * (2 * W) ^ (J * k + S) ≤
          (Real.exp 150 * Real.sqrt W) ^ (2 * k * J) := by
…

theorem OAI.TwoPointCorrelations.eventually_good_moment_with_padding line 81

Source documentation

Restore the normalization factor from the padding sum.

theorem eventually_good_moment_with_padding (W : ℝ) (hW : 1 ≤ W) :
    ∀ᶠ L : ℝ in atTop, ∀ J k S : ℕ, ∀ K : ℝ,
      1 ≤ J → L / 2 ≤ (k : ℝ) → (S : ℝ) ≤ L ^ (1 / 4 : ℝ) → 0 ≤ K →
      Real.exp (108 * L) * (2 : ℝ) ^ (4 * k * J + 2 * S) *
        Real.exp (64 * k * J) * K ^ (2 * k) * (2 * W) ^ (J * k + S) ≤
          (K * (Real.exp 150 * Real.sqrt W) ^ J) ^ (2 * k) := by
…