OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateLogProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplateCoefficient_bulk_log_product_lower line 13

   Source documentation

   The original weighted coefficient forces the full bulk product above its log-bin boundary before any compensation product is included.

   theorem movingTemplateCoefficient_bulk_log_product_lower {σ : Type} [Fintype σ]
       (value tier : σ → ℕ) (hvalue : ∀ a, 0 < value a) (k : ℕ)
       (outside : List ℕ) (cb cd : ℝ) (μ : ℕ → σ → ℝ)
       (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (y : MovingRegularSlot n r m → σ) (hn : n ≤ k)
       (hsmall : ∀ j : TreeLeafIndex n × Fin r, tier (y (j.1, .inl j.2)) ≠ k)
       (hbulk : ∀ j : TreeLeafIndex n × Fin m, tier (y (j.1, .inr j.2)) = k)
       (XL XR : ℕ)
       (h : movingTemplateCoefficient value outside μ childBound pivotBound V
         (fun x s => (movingBulkLeafLogWeight value tier k outside cb cd x.data : ℂ) * F x s)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingTemplateCoefficient, OAI.Ostmann.movingBulkLeafLogWeight

2. theorem OAI.Ostmann.movingTemplateCoefficient_log_product_lower line 47

   Source documentation

   The original weighted coefficient forces the full bulk product above its log-bin boundary. Small-slot primes only increase the regular modulus.

   theorem movingTemplateCoefficient_log_product_lower {σ : Type} [Fintype σ]
       (value tier : σ → ℕ) (hvalue : ∀ a, 0 < value a) (k : ℕ)
       (outside : List ℕ) (cb cd : ℝ) (μ : ℕ → σ → ℝ)
       (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (y : MovingRegularSlot n r m → σ) (hn : n ≤ k)
       (hsmall : ∀ j : TreeLeafIndex n × Fin r, tier (y (j.1, .inl j.2)) ≠ k)
       (hbulk : ∀ j : TreeLeafIndex n × Fin m, tier (y (j.1, .inr j.2)) = k)
       (XL XR : ℕ)
       (h : movingTemplateCoefficient value outside μ childBound pivotBound V
         (fun x s => (movingBulkLeafLogWeight value tier k outside cb cd x.data : ℂ) * F x s)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingTemplateCoefficient, OAI.Ostmann.movingBulkLeafLogWeight