MRTShortMeanRate.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Independent height and short-length thresholds for the final scalar MRT rate. The density remains linear and the logarithmic energy error has the published exponent after taking its square root.

lemma OAI.TwoPointCorrelations.mrt_three_square_envelope line 14

lemma OAI.TwoPointCorrelations.mrt_first_kernel_square_rate line 26

Source documentation

The elementary kernel and finite endpoint terms fit the square of loglog(H)/log(H), with a threshold only on the short length.

lemma mrt_first_kernel_square_rate (A : ℕ) (hA : 500000 ≤ A) :
    ∀ᶠ H : ℝ in atTop,
      0 ≤ Real.log (Real.log H)/Real.log H ∧
      0 ≤ Real.log (minorArcFirstLower A H)/Real.log (minorArcFirstUpper H) ∧
      Real.log (minorArcFirstLower A H)/Real.log (minorArcFirstUpper H)  ≤
        (10*(A:ℝ))*(Real.log (Real.log H)/Real.log H) ∧
      33792*Real.exp 1*(mrtBaseResolution (minorArcFirstLower A H)
        (minorArcFirstUpper H) (1/100))⁻¹ + 2*(minorArcFirstLower A H)⁻¹ +
      1024*Real.exp 2*(mrtBaseResolution (minorArcFirstLower A H)
        (minorArcFirstUpper H) (1/100))⁻¹*(1+minorArcFirstUpper H/H)  ≤
        (33792*Real.exp 1+2+2048*Real.exp 2)*(Real.log (Real.log H)/Real.log H)^2 ∧
      1/H^2  ≤  (Real.log (Real.log H)/Real.log H)^2 := by
…

Mentions: OAI.TwoPointCorrelations.minorArcFirstLower, OAI.TwoPointCorrelations.minorArcFirstUpper, OAI.TwoPointCorrelations.mrtBaseResolution

theorem OAI.TwoPointCorrelations.mrt_short_mean_rate line 73

Source documentation

The exact scalar expression in halasz_actual_short_mean has the required rate with independent absolute-scale and short-length thresholds.

theorem mrt_short_mean_rate (A : ℕ) (hA : 500000 ≤ A) (C₁ C₂ : ℝ)
    (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) :
    ∃ C L₀ H₀ : ℝ, 0<C ∧ 1 ≤ L₀ ∧ 1 ≤ H₀ ∧
      ∀ L : ℝ, L₀ ≤ L → ∀ H : ℝ, H₀ ≤ H → ∀ M : ℝ,
      Real.sqrt ((139968/(2*Real.pi)) *
        (12*(C₁*((Real.log (minorArcFirstLower A H)/Real.log (minorArcFirstUpper H))^2+
            Real.exp (-M)+Real.log L/L^(1/100:ℝ)) +
          33792*Real.exp 1*(mrtBaseResolution (minorArcFirstLower A H)
            (minorArcFirstUpper H) (1/100))⁻¹ + 2*(minorArcFirstLower A H)⁻¹ +
          1024*Real.exp 2*(mrtBaseResolution (minorArcFirstLower A H)
            (minorArcFirstUpper H) (1/100))⁻¹*(1+minorArcFirstUpper H/H)) +
          128*Real.exp 1/H^2)) +
…

Mentions: OAI.TwoPointCorrelations.minorArcFirstLower, OAI.TwoPointCorrelations.minorArcFirstUpper, OAI.TwoPointCorrelations.mrtBaseResolution