MovingNormalizedEnergyBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic energy bounds the original normalized giant average

theorem OAI.Ostmann.movingPrimeCore_normalized_energy_bound line 13

Source documentation

The four unit-rectangle energy bounds give the full original giant law. The factors from the two harmonic normalizations are retained explicitly.

theorem movingPrimeCore_normalized_energy_bound {σ I B : Type}
    [Fintype σ] [Fintype B] (q : I → ℕ) [∀ i, Fact (q i).Prime]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ)
    (childBound pivotBound V : ℕ → ℕ) (f : ℤ → ℂ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (hφ : ∀ x, 0 ≤ φ x)
    (Bφ Dφ : ℝ) (hBφ : 0 ≤ Bφ) (hDφ : 0 ≤ Dφ)
    (hφnorm : ∀ x, |φ x| ≤ Bφ) (hlip : ∀ x y, |φ x - φ y| ≤ Dφ * |x - y|)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0) (G : ℕ → ℝ)
    (n m : ℕ) (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (hsmall : ∀ i ∈ flattenMovingSlots n small, i ∉ Set.range slot)
    (hν : ∀ b a, 0 ≤ ν b a) (hmass : ∀ b, ∑ a, ν b a = 1)
…

Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.flattenMovingSlots