OAI/NumberTheory/Ostmann/Arithmetic/MovingRecursiveProductBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingProductExponent line 11

   Source documentation

   The logarithmic product budget left after each common pivot is removed.

   noncomputable def movingProductExponent (T : ℕ → ℝ) (W : ℝ) : ℕ → ℝ
     | 0 => W
     | n + 1 => 2 * (movingProductExponent T W n - T n)

2. theorem OAI.Ostmann.remove_positive_product line 15
3. theorem OAI.Ostmann.movingNaturalProduct_append_leaves line 24
4. theorem OAI.Ostmann.movingSupportedSampledWeight_product_bound line 40

   Source documentation

   This bound is proved on the original sampled histories, before summing any frequencies. The inserted giants may be arbitrary positive integers.

   theorem movingSupportedSampledWeight_product_bound {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (T : ℕ → ℝ) (W : ℝ)
       (hF : ∀ s small XL XR,
         F ⟨0, .leaf s small, XL, XR⟩ s ≠ 0 →
           ((XL * XR * MovingSlotReversal.naturalProduct value small : ℕ) : ℝ) ≤ Real.exp W)
       (hmin : ∀ n (a : TreeLeafTuple (Fin 4 → σ) n),
         movingCompensationPrior (μ n) n a ≠ 0 → ∀ p : ℕ, 0 < p →
         φ (Real.log p - G (n + 1)) ≠ 0 →
         Real.exp (T n) ≤ (p * MovingSlotReversal.naturalProduct value
           (flattenMovingSlots n (movingCompensationSlots n a)) : ℕ))
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensationPrior, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingCompensationSlots

5. theorem OAI.Ostmann.movingFrequencyCoefficient_recursive_product_bound line 123

   Source documentation

   Summing descendants cannot create support outside the inherited product window. This is the coefficient used by the original arithmetic comparison.

   theorem movingFrequencyCoefficient_recursive_product_bound {σ I : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi W : ℝ) (hX : 0 < X) (hwindow : X * hi ≤ Real.exp W)
       (φ : ℝ → ℝ) (G T : ℕ → ℝ)
       (hmin : ∀ n (a : TreeLeafTuple (Fin 4 → σ) n),
         movingCompensationPrior (μ n) n a ≠ 0 → ∀ p : ℕ, 0 < p →
         φ (Real.log p - G (n + 1)) ≠ 0 →
         Real.exp (T n) ≤ (p * MovingSlotReversal.naturalProduct value
           (flattenMovingSlots n (movingCompensationSlots n a)) : ℕ))
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensationPrior, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingCompensationSlots