BulkAbsoluteIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the nonnegative arithmetic norm under the original Page density

theorem OAI.Ostmann.bulk_absolute_integral_bound line 15

Source documentation

The absolute residue average is integrated with the true harmonic box volume. The Page factors remain inside the arithmetic norm estimate.

theorem bulk_absolute_integral_bound {J : Type*} [Fintype J]
    (P : PublishedProgressionInput) (Q M : ℕ) [NeZero M]
    (u v : J → ℝ) (hu : ∀ j, 0 < u j)
    (K : BulkIntegrand J) (a : (J → (ZMod M)ˣ) → ℂ) (W A : ℝ)
    (hW : 0 ≤ W) (hK : ∀ y, ‖K y‖ ≤ W)
    (hA : ∀ y : J → ℝ, (∀ j, y j ∈ Set.Ioc (u j) (v j)) →
      (Fintype.card (J → (ZMod M)ˣ) : ℝ)⁻¹ *
        ∑ z, ‖a z * ∏ j, pageGiantWeight P Q M (z j).val.val (y j)‖ ≤ A) :
    ‖∑ z : J → (ZMod M)ˣ, ∫ y, (K.constMul (a z)) y ∂Measure.pi (fun j =>
      primeGiantMeasure P Q M (z j).val.val (u j) (v j))‖ ≤
      (W * A) * ∏ j, ∫ x in Set.Ioc (u j) (v j), (x : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.BulkIntegrand, OAI.Ostmann.pageGiantWeight, OAI.Ostmann.primeGiantMeasure

theorem OAI.Ostmann.bulk_absolute_mixture_bound line 68

Source documentation

Sum all original boxes with their unchanged reciprocal-prime normalizers.

theorem bulk_absolute_mixture_bound {J C : Type*} [Fintype J] [Fintype C]
    (P : PublishedProgressionInput) (Q M : ℕ) [NeZero M]
    (u v : J → C → ℝ) (hu : ∀ j c, 0 < u j c)
    (Z : J → ℝ) (hZ : ∀ j, 0 ≤ Z j)
    (hmass : ∀ j, Z j * ∑ c, ∫ x in Set.Ioc (u j c) (v j c), (x : ℝ)⁻¹ ≤ 2)
    (K : BulkIntegrand J) (a : (J → (ZMod M)ˣ) → ℂ) (W A : ℝ)
    (hW : 0 ≤ W) (hA0 : 0 ≤ A) (hK : ∀ y, ‖K y‖ ≤ W)
    (hA : ∀ y : J → ℝ, (∀ j, 0 ≤ y j) →
      (Fintype.card (J → (ZMod M)ˣ) : ℝ)⁻¹ *
        ∑ z, ‖a z * ∏ j, pageGiantWeight P Q M (z j).val.val (y j)‖ ≤ A) :
    ‖∑ z : J → (ZMod M)ˣ, ∫ y, (K.constMul (a z)) y ∂Measure.pi (fun j =>
      bulkCellMixture (Z j) (fun c => primeGiantMeasure P Q M (z j).val.val (u j c) (v j c)))‖ ≤
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.BulkIntegrand, OAI.Ostmann.pageGiantWeight, OAI.Ostmann.bulkCellMixture, OAI.Ostmann.primeGiantMeasure