OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSetSampling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A bounded measurable frequency set can be sampled in two separated classes. Sample points stay in the original set, so its large-value witnesses are preserved without taking a neighbourhood or differentiating them.

  1. lemma OAI.TwoPointCorrelations.mrt_unit_cell_sample line 14
  2. lemma OAI.TwoPointCorrelations.mrt_cell_sample_injective line 46
  3. lemma OAI.TwoPointCorrelations.mrt_cell_sample_separated line 63
  4. theorem OAI.TwoPointCorrelations.mrt_set_integral_of_samples line 88

    Source documentation

    A uniform bound on all separated samples gives a bound on the actual set integral, with the sample points still lying in that set.

    theorem mrt_set_integral_of_samples (G : ℝ → ℝ) (hG : Continuous G)
    (hG0 : ∀ t, 0 ≤ G t) {E : Set ℝ} (hE : MeasurableSet E)
    {T B : ℝ} (hT : 0 ≤ T) (hET : E ⊆ Set.Ioc (-T) T)
    (hsamples : ∀ S : Finset ℝ, (∀ t ∈ S, t ∈ E) →
      (∀ t ∈ S, ∀ s ∈ S, t≠s → 1 ≤ |t-s|) → ∑ t ∈ S, G t ≤ B) :
    (∫ t in E, G t) ≤ 4*B := by
…