OAI/NumberTheory/JointDickman/Amplification/SeparatedCellIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.unit_measure_integral_sample line 11
2. theorem OAI.JointDickman.separated_cell_integral_bound line 23

   Source documentation

   Each cell has measure at most one and cells in the family are separated. The sample bound is therefore also a bound for the sum of their integrals.

   theorem separated_cell_integral_bound (I : Finset ℕ) (E : ℕ → Set ℝ)
       (S : Set ℝ) (F : ℝ → ℝ) (B : ℝ)
       (hF : ∀ i ∈ I, IntegrableOn F (E i)) (hF0 : ∀ x ∈ S, 0 ≤ F x)
       (hES : ∀ i ∈ I, E i ⊆ S)
       (hEf : ∀ i ∈ I, volume (E i) ≠ ⊤)
       (hE1 : ∀ i ∈ I, volume.real (E i) ≤ 1)
       (hsep : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → ∀ x ∈ E i, ∀ y ∈ E j, 1 ≤ |x-y|)
       (hsample : ∀ U : Finset ℝ, (∀ x ∈ U, x ∈ S) →
         (∀ x ∈ U, ∀ y ∈ U, x ≠ y → 1 ≤ |x-y|) → (∑ x ∈ U, F x) ≤ B) :
       (∑ i ∈ I, ∫ t in E i, F t) ≤ B := by
   …