OAI/NumberTheory/Ostmann/Arithmetic/MovingBulkLogProductLower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingBulkListLogWeight_product_lower line 12
2. theorem OAI.Ostmann.movingBulkTreeLogWeight_product_lower line 41

   Source documentation

   Every original leaf supplies its own product lower bound. Multiplication therefore gives the full 2^n exponent, with no distinctness assumption.

   theorem movingBulkTreeLogWeight_product_lower {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ a, 0 < value a) (outside : List ℕ) (cb cd : ℝ)
       (n m : ℕ) (slot : TreeLeafIndex n × Fin m → σ)
       (h : treeLeafProduct n (treeLeafMap (movingBulkListLogWeight value outside cb cd) n
         (bulkSlotLeaves n m slot)) ≠ 0) :
       Real.exp ((2 ^ n : ℕ) * (cb - 1)) ≤ ((∏ i, value (slot i) : ℕ) : ℝ) := by
   …

   Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.treeLeafProduct, OAI.Ostmann.treeLeafMap, OAI.Ostmann.movingBulkListLogWeight, OAI.Ostmann.bulkSlotLeaves

3. theorem OAI.Ostmann.movingFrequencyCoefficient_log_product_lower line 69

   Source documentation

   The actual weighted Fourier coefficient can be nonzero only above the product cutoff. This uses the exact coefficient factorization, not an extra support hypothesis on a surrogate coefficient.

   theorem movingFrequencyCoefficient_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 m : ℕ) (s : ℤ)
       (small : TreeLeafTuple (List σ) n) (slot : TreeLeafIndex n × Fin m → σ)
       (hn : n ≤ k) (hsmall : ∀ i ∈ flattenMovingSlots n small, tier i ≠ k)
       (hbulk : ∀ i ∈ flattenMovingSlots n (bulkSlotLeaves n m slot), tier i = k)
       (XL XR : ℕ)
       (h : movingFrequencyCoefficient 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.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.bulkSlotLeaves, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.movingBulkLeafLogWeight

4. theorem OAI.Ostmann.movingFrequencyCoefficient_bulk_log_norm_le line 90

   Source documentation

   Pointwise removal is valid for one unsymmetrized coefficient. This is used only after the harmonic diagonal has reduced to one-branch energy.

   theorem movingFrequencyCoefficient_bulk_log_norm_le {σ : Type} [Fintype σ]
       (value tier : σ → ℕ) (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
       (μ : ℕ → σ → ℝ) (hμ : ∀ j a, μ j a ≠ 0 → tier a = j)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
       (small bulk : TreeLeafTuple (List σ) n)
       (hn : n ≤ k) (hsmall : ∀ i ∈ flattenMovingSlots n small, tier i ≠ k)
       (hbulk : ∀ i ∈ flattenMovingSlots n bulk, tier i = k) (XL XR : ℕ) :
       ‖movingFrequencyCoefficient value outside μ childBound pivotBound V
         (fun x s => (movingBulkLeafLogWeight value tier k outside cb cd x.data : ℂ) * F x s)
         φ G n s small bulk XL XR‖ ≤
       ‖movingFrequencyCoefficient value outside μ childBound pivotBound V F
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingFrequencyCoefficient, OAI.Ostmann.movingBulkLeafLogWeight