MovingPrimeInternalNorm.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Retaining the internal line factor in the two-prime environment

theorem OAI.Ostmann.internal_sum_norm line 10
theorem OAI.Ostmann.unit_pair_average_le_twice_mixed line 26
theorem OAI.Ostmann.movingInternalPrimeAverage_norm_le line 74
Source documentation
Restricting the first giant to units costs at most two at each distinct internal prime, while retaining the full simultaneous line probability.
```
theorem movingInternalPrimeAverage_norm_le {σ : Type*} {n : ℕ}
    (value : σ → ℕ) (T : Bool → MovingSlotData σ n) (p : ℕ) [Fact p.Prime] :
    ‖movingInternalPrimeAverage value T p‖ ≤ 2 * movingInternalLineProbability value T p := by
…
```
Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingInternalPrimeAverage, OAI.Ostmann.movingInternalLineProbability

theorem OAI.Ostmann.movingInternalPrimeAverage_product_norm_le line 90

Source documentation

Only a fixed factor per equality class is paid, and every class retains its original inverse-prime line probability.

theorem movingInternalPrimeAverage_product_norm_le {σ : Type*} {n : ℕ}
    (value : σ → ℕ) (T : Bool → MovingSlotData σ n)
    (P : Finset ℕ) [∀ p : P, Fact p.val.Prime] :
    ‖∏ p : P, movingInternalPrimeAverage value T p.val‖ ≤
      (2 : ℝ) ^ P.card * ∏ p : P, movingInternalLineProbability value T p.val := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingInternalPrimeAverage, OAI.Ostmann.movingInternalLineProbability