OAI/NumberTheory/TwoPoint/Walks/RetainedComplexBlock.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.retainedComplexPrimeEdge line 14
2. lemma OAI.TwoPointCorrelations.retainedComplexPrimeEdge_support line 27
3. def OAI.TwoPointCorrelations.retainedComplexBlock line 43
4. lemma OAI.TwoPointCorrelations.retainedComplexBlock_eq_edges line 54
5. lemma OAI.TwoPointCorrelations.retainedComplexBlock_eq_blocks line 114
6. theorem OAI.TwoPointCorrelations.retainedComplexBlock_prefix_bound line 128

   Source documentation

   The prefix transfer is valid for arbitrary complex factors. The row and block bounds are separate estimates, so no positivity of either factor is required.

   theorem retainedComplexBlock_prefix_bound {J : ℕ} (P : Fin J → Finset ℕ)
       (M R N : ℕ) (Q Qp : Finset ℕ) (u : ℕ → ℝ) (eligible : ℕ → ℕ → Prop)
       (L K W : ℝ) (extra : ℕ → ℤ → Prop) (h : ℕ)
       (gate : ℕ → ℤ → ℤ → Prop) (keep : ℤ → Prop) (F G : ℤ → ℂ)
       (hM : 0 < M) (hN : 0 < N) (B C : ℝ) (hC : 0 ≤ C)
       (hr : ∀ e : ((j : Fin J) → P j) × Q, retainedPrimeStep eligible h e ≤ R)
       (hrow : ∀ n : ℕ, 0 < n →
         (∑ e : ((j : Fin J) → P j) × Q,
           ‖retainedComplexPrimeEdge P Q Qp u eligible L K W extra h gate keep F G e n
             ((n : ℤ) + retainedPrimeStep eligible h e)‖) ≤ C)
       (havg : uniformAverage (fun t : Fin N =>
         ‖retainedComplexBlock P M Q Qp u eligible L K W extra h gate keep F G t.val‖) ≤ B) :
   …

   Mentions: OAI.TwoPointCorrelations.retainedPrimeStep, OAI.TwoPointCorrelations.retainedComplexPrimeEdge, OAI.TwoPointCorrelations.uniformAverage, OAI.TwoPointCorrelations.retainedComplexBlock