OAI/NumberTheory/Ostmann/Arithmetic/MovingMaskedTemplateEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingRestoredCompensationProduct line 11
2. theorem OAI.Ostmann.movingRestoredCompensationProduct_restore line 15
3. def OAI.Ostmann.movingMaskedTemplateKernel line 22
4. theorem OAI.Ostmann.movingMaskedTemplateKernel_restore line 36
5. def OAI.Ostmann.movingMaskedTemplateEnergy line 58
6. theorem OAI.Ostmann.movingMaskedTemplateKernel_nonneg line 72
7. theorem OAI.Ostmann.movingMaskedTemplateEnergy_weight_le line 89

   Source documentation

   A bound on the original support suffices: no support is conditioned into or removed from the independent restored law.

   theorem movingMaskedTemplateEnergy_weight_le
       (P Pg I : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (outside : List ℕ) (μ : ℕ → P → ℝ)
       (hμ : ∀ j a, 0 ≤ μ j a)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (φ : ℝ → ℝ) (hφ : ∀ t, 0 ≤ φ t) (G : ℕ → ℝ) (n r m : ℕ)
       (Q : MovingRegularSlot n r m → Finset ℕ) (greg : ∀ q : ℕ, ZMod q → ℂ)
       (weight : (MovingRegularSlot n (4 + r) m → P) → ℝ) (B : ℝ)
       (hweight : ∀ x, (∏ i, movingTemplateRestoredPrior n r m (μ n)
         (fun i => primeSubsetPrior P (Q i)) i (x i)) ≠ 0 → weight x ≤ B) :
       movingMaskedTemplateEnergy P Pg I hP outside μ childBound pivotBound V F φ G n r m Q greg weight ≤
         B * movingMaskedTemplateEnergy P Pg I hP outside μ childBound pivotBound V F φ G n r m Q greg (fun _ => 1) := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateRestoredPrior, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.movingMaskedTemplateEnergy

8. theorem OAI.Ostmann.movingRestoredCompensationProduct_le_exp line 134

   Source documentation

   The compensation product is bounded using only the support of the same original prior. All four draws at every leaf are counted.

   theorem movingRestoredCompensationProduct_le_exp
       (P : Finset ℕ) (μ : P → ℝ) (n r m : ℕ)
       (ν : MovingRegularSlot n r m → P → ℝ) (b : ℝ)
       (hb : ∀ a, μ a ≠ 0 → (a : ℝ) ≤ Real.exp b)
       (x : MovingRegularSlot n (4 + r) m → P)
       (hx : (∏ i, movingTemplateRestoredPrior n r m μ ν i (x i)) ≠ 0) :
       (movingRestoredCompensationProduct Subtype.val n r m x : ℝ) ≤
         Real.exp (((2 ^ n * 4 : ℕ) : ℝ) * b) := by
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateRestoredPrior, OAI.Ostmann.movingRestoredCompensationProduct