OAI/NumberTheory/Ostmann/Arithmetic/MovingRecursiveTemplateCaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingCellPivotExponent line 10
2. theorem OAI.Ostmann.movingFrequencyCoefficient_recursive_cell_cap line 15

   Source documentation

   Every compensation prior is the original prior. Only its actual nonzero support is used in the lower bound; no renormalization is performed.

   theorem movingFrequencyCoefficient_recursive_cell_cap {σ 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 c : ℕ → ℝ) (hout : ∀ t, 1 ≤ |t| → φ t = 0)
       (hμ : ∀ j x, μ j x ≠ 0 → Real.exp (c j - 1) ≤ (value x : ℝ))
       (n : ℕ) (a : TreeLeafTuple (Fin 4 → σ) n)
       (ha : movingCompensationPrior (μ n) n a ≠ 0)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensationPrior

3. theorem OAI.Ostmann.movingTemplateCoefficient_recursive_cell_cap line 65

   Source documentation

   The product bound required by the Cauchy--Schwarz transfer now follows at any depth from the terminal cutoff and the selected compensation cells.

   theorem movingTemplateCoefficient_recursive_cell_cap {σ 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 c : ℕ → ℝ) (hout : ∀ t, 1 ≤ |t| → φ t = 0)
       (hμ : ∀ j x, μ j x ≠ 0 → Real.exp (c j - 1) ≤ (value x : ℝ))
       (n r m : ℕ) (u : TreeLeafIndex n × Fin 4 → σ) (hu : (∏ i, μ n (u i)) ≠ 0)
       (s : ℤ) (y : MovingRegularSlot n r m → σ) (p XR : ℕ)
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot