OAI/NumberTheory/Ostmann/Construction/FiniteMatchedWindow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.finite_prime_prior_product_lower line 10
2. theorem OAI.Ostmann.finite_matched_window_eq line 23

   Source documentation

   The normalizing factor is pulled outside all H/Y summation. The inserted cutoff follows from the original cell endpoints whenever the prior is nonzero.

   theorem finite_matched_window_eq {H Y : Type*} [Fintype H] [Fintype Y]
       (P : Finset ℕ) (Q : H ⊕ Y → Finset ℕ) (e : Equiv.Perm H)
       (F : (H ⊕ Y → P) → ℂ) (lo : H → ℝ) (hlo : ∀ h, 0 ≤ lo h)
       (hcell : ∀ h p, p ∈ Q (.inl h) → lo h ≤ (p : ℝ))
       (Z : ℝ) (hZ : 0 < Z) (hscale : Z ≤ ∏ h, lo h) :
       (∑ x : H ⊕ Y → P,
         ((∏ i, primeSubsetPrior P (Q i) (x i) : ℝ) : ℂ) *
         ((∏ h, primeSubsetPrior P (Q (.inl h)) (x (.inl (e h))) : ℝ) : ℂ) * F x) =
       (((∏ h, (∑ p ∈ Q (.inl h), (p : ℝ)⁻¹)⁻¹) * Z⁻¹ : ℝ) : ℂ) *
         ∑ x : H ⊕ Y → P, ((Z / (∏ h, (x (.inl h) : ℝ)) : ℝ) : ℂ) *
           (if Z ≤ ∏ h, (x (.inl h) : ℝ) then
             ((∏ i, primeSubsetPrior P (Q i) (x i) : ℝ) : ℂ) *
   …

   Mentions: OAI.Ostmann.primeSubsetPrior

3. def OAI.Ostmann.retainedHWord line 54
4. theorem OAI.Ostmann.retainedHWord_length line 57
5. theorem OAI.Ostmann.retainedHWord_prod line 61
6. theorem OAI.Ostmann.finite_matched_window_bound line 65