MovingFrequencyPrimeSquare.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual coefficient square inside the original two prime intervals

theorem OAI.Ostmann.movingFrequencyCoefficient_original_prime_square line 13

Source documentation

Expanding the square and exchanging the finite prime sums introduces exactly the two independent descendant histories used in the arithmetic norm.

theorem movingFrequencyCoefficient_original_prime_square {σ I : Type} [Fintype σ]
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value : σ → ℕ) (outside : List ℕ)
    (μ : ℕ → σ → ℝ) (childBound pivotBound V : ℕ → ℕ)
    (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (s : ℤ) (small bulk : TreeLeafTuple (List σ) n) (u v r w : ℝ) :
    let W := fun (a : MovingDescendantFrequencyIndex V n) (x y : ℝ) =>
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingDescendantFrequencyIndex

def OAI.Ostmann.sameRootScheduledPairEmbedding line 49
Source documentation
Two descendant histories in a coefficient square share their root. Their inclusion in the full pair of scheduled histories is injective.
```
def sameRootScheduledPairEmbedding (V : ℕ → ℕ) (n : ℕ) :
    (transferFrequencyRange (V n) ×
      (MovingDescendantFrequencyIndex V n × MovingDescendantFrequencyIndex V n)) ↪
    (ScheduledFrequencyIndex V n × ScheduledFrequencyIndex V n) where
…
```
Mentions: OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.MovingDescendantFrequencyIndex, OAI.Ostmann.ScheduledFrequencyIndex

theorem OAI.Ostmann.same_root_scheduled_pair_sum_le line 71

Source documentation

Enlarging only the shared-root restriction costs no factor. This is used after the exact original prime-pair expansion of each coefficient square.

theorem same_root_scheduled_pair_sum_le (V : ℕ → ℕ) (n : ℕ)
    (F : ScheduledFrequencyIndex V n → ScheduledFrequencyIndex V n → ℝ)
    (hF : ∀ a b, 0 ≤ F a b) :
    (∑ s : transferFrequencyRange (V n), ∑ a : MovingDescendantFrequencyIndex V n,
      ∑ b : MovingDescendantFrequencyIndex V n,
        F ((scheduledFrequencyRootEquiv V n).symm (s, a))
          ((scheduledFrequencyRootEquiv V n).symm (s, b))) ≤
    ∑ a : ScheduledFrequencyIndex V n, ∑ b : ScheduledFrequencyIndex V n, F a b := by
…

Mentions: OAI.Ostmann.ScheduledFrequencyIndex, OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.MovingDescendantFrequencyIndex, OAI.Ostmann.scheduledFrequencyRootEquiv