MovingOriginalLogGiantWeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual terminal log factors in the original giant coefficient

theorem OAI.Ostmann.movingOriginalGiantWeight_bulk_log line 13

Source documentation

The terminal weights factor from the full original recursion, with its sharp windows, cutoffs and support retained.

theorem movingOriginalGiantWeight_bulk_log {σ I : Type*}
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value tier : σ → ℕ)
    (k : ℕ) (outside : List ℕ) (cb cd : ℝ) (childBound pivotBound : ℕ → ℕ)
    (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (XL XR : ℕ) :
    movingOriginalGiantWeight q value childBound pivotBound
        (fun T s => (movingBulkLeafLogWeight value tier k outside cb cd T : ℂ) * F T s)
        E g Dq S ψ X lo hi φ G T t XL XR =
      (movingBulkTreeLogWeight value tier k outside cb cd T : ℂ) *
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingOriginalGiantWeight, OAI.Ostmann.movingBulkLeafLogWeight, OAI.Ostmann.movingBulkTreeLogWeight

theorem OAI.Ostmann.movingOriginalGiantWeight_pair_bulk_log line 41

Source documentation

Both original branches retain their own terminal grouping inside the common prime average; the fixed outside profile is the only scalar extracted.

theorem movingOriginalGiantWeight_pair_bulk_log {σ I : Type*}
    (q : I → ℕ) [∀ i, Fact (q i).Prime] (value tier : σ → ℕ)
    (hvalue : ∀ a, 0 < value a) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
    (childBound pivotBound : ℕ → ℕ)
    (F : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
    (E : Bool → {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : Bool → ∀ i, (ZMod (q i))ˣ) (S : Finset I)
    (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    {n : ℕ} (T : Bool → MovingSlotData σ n) (t : Bool → FrequencyTree ℤ n) (XL XR : ℕ) :
    let slots := Fin.append
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree