MRTCommonDistance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A single original-cutoff distance condition supplies both dyadic kernel endpoints. The loss is absolute and is truncated at zero.

theorem OAI.TwoPointCorrelations.mrt_common_distance_lower_bound line 14

Source documentation

The same distance lower bound, with one fixed loss, holds at all endpoints 2*k for N≤k≤2*N, hence in particular at 2*N and 4*N.

theorem mrt_common_distance_lower_bound : ∃ K : ℝ, 0≤K ∧
    ∀ N : ℕ, 1≤N → ∀ F : ℕ → ℂ, OneBounded F → ∀ M : ℝ,
      (∀ v : ℝ, |v|≤4*N → M≤squaredDistance F (mrtArchimedeanTwist v) (4*N)) →
      ∀ k∈Icc N (2*N), ∀ v : ℝ, |v|≤2*k →
        max 0 (M-K)≤squaredDistance F (mrtArchimedeanTwist v) (2*k) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist

theorem OAI.TwoPointCorrelations.mrt_two_endpoint_distance line 39

Source documentation

The two actual endpoints used by the logarithmic kernel have one uniform original-cutoff lower bound.

theorem mrt_two_endpoint_distance : ∃ K : ℝ, 0≤K ∧
    ∀ N : ℕ, 1≤N → ∀ F : ℕ → ℂ, OneBounded F → ∀ M : ℝ,
      (∀ v : ℝ, |v|≤4*N → M≤squaredDistance F (mrtArchimedeanTwist v) (4*N)) →
      ∀ k∈({N,2*N}:Finset ℕ), ∀ v : ℝ, |v|≤2*k →
        max 0 (M-K)≤squaredDistance F (mrtArchimedeanTwist v) (2*k) := by
…

Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist