OAI/NumberTheory/JointDickman/Amplification/IntegralFromSamples.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.unit_grid_cover line 10
2. lemma OAI.JointDickman.unit_grid_same_parity_separated line 33
3. theorem OAI.JointDickman.integral_le_twice_separated_samples line 52

   Source documentation

   A unit grid splits into two separated classes. No regularity of the frequency set beyond measurability is required.

   theorem integral_le_twice_separated_samples (S : Set ℝ) (hSm : MeasurableSet S)
       (F : ℝ → ℝ) (hF0 : ∀ x ∈ S, 0 ≤ F x) (a : ℝ) (M : ℕ)
       (hS : S ⊆ Set.Ico a (a+M)) (hF : IntegrableOn F (Set.Ico a (a+M))) (B : ℝ)
       (hsample : ∀ U : Finset ℝ, (∀ x ∈ U, x ∈ S) →
         (∀ x ∈ U, ∀ y ∈ U, x ≠ y → 1 ≤ |x-y|) → (∑ x ∈ U, F x) ≤ B) :
       (∫ x in S, F x) ≤ 2*B := by
   …

4. theorem OAI.JointDickman.bounded_integral_le_twice_samples line 116

   Source documentation

   The bounded-frequency form used for Mellin polynomials.

   theorem bounded_integral_le_twice_samples (S : Set ℝ) (hSm : MeasurableSet S)
       (F : ℝ → ℝ) (hF : Continuous F) (hF0 : ∀ x ∈ S, 0 ≤ F x)
       {T : ℝ} (_hT : 0 ≤ T) (hS : S ⊆ Set.Ioc (-T) T) (B : ℝ)
       (hsample : ∀ U : Finset ℝ, (∀ x ∈ U, x ∈ S) →
         (∀ x ∈ U, ∀ y ∈ U, x ≠ y → 1 ≤ |x-y|) → (∑ x ∈ U, F x) ≤ B) :
       (∫ x in S, F x) ≤ 2*B := by
   …