MRTSampleCost.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Optimizing the actual finite sample moment at the first power reaching the frequency height. The estimates apply to the last-band and additional large-prime witnesses without replacing their literal sample cost.

theorem OAI.TwoPointCorrelations.mrt_short_prime_sample_cost_le line 14
Source documentation
Once Y^r reaches the height, all ambient-height and rounding factors are absorbed into an explicit exponential in the moment order.
```
theorem mrt_short_prime_sample_cost_le {Y V T : ℝ} (hY : 1 ≤ Y)
    (hV : 0 < V) {r : ℕ} (hTr : T ≤ Y^r) :
    mrtShortPrimeSampleCost Y V T r ≤
      24*Real.exp 1*(2+((r:ℝ)*Real.log (4*Y))^2)*(8*(r:ℝ))^r/V^(2*r) := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtShortPrimeSampleCost

theorem OAI.TwoPointCorrelations.mrt_short_prime_sample_cost_chosen line 60

Source documentation

The exact ceiling moment realizes the preceding height balance.

theorem mrt_short_prime_sample_cost_chosen {Y V T : ℝ} (hY : 1 < Y)
    (hV : 0 < V) (hT : 1 ≤ T) :
    mrtShortPrimeSampleCost Y V T (mrtAmplificationOrder Y T) ≤
      24*Real.exp 1*
        (2+((mrtAmplificationOrder Y T:ℝ)*Real.log (4*Y))^2)*
        (8*(mrtAmplificationOrder Y T:ℝ))^(mrtAmplificationOrder Y T)/
        V^(2*mrtAmplificationOrder Y T) :=
…

Mentions: OAI.TwoPointCorrelations.mrtShortPrimeSampleCost, OAI.TwoPointCorrelations.mrtAmplificationOrder

theorem OAI.TwoPointCorrelations.mrt_short_prime_sample_cost_exp line 70

Source documentation

An exponential form suitable for the small fixed extra-band exponent.

theorem mrt_short_prime_sample_cost_exp {Y V T : ℝ} (hY : 1 < Y)
    (hV : 0 < V) (hT : 1 < T) :
    mrtShortPrimeSampleCost Y V T (mrtAmplificationOrder Y T) ≤
      24*Real.exp 1*
        (2+((mrtAmplificationOrder Y T:ℝ)*Real.log (4*Y))^2)*
        Real.exp ((mrtAmplificationOrder Y T:ℝ)*
          (Real.log (8*(mrtAmplificationOrder Y T:ℝ))-2*Real.log V)) := by
…

Mentions: OAI.TwoPointCorrelations.mrtShortPrimeSampleCost, OAI.TwoPointCorrelations.mrtAmplificationOrder