OAI/NumberTheory/Ostmann/Construction/SelectedCompensationPrior.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.selectedCompensationPrior line 10
2. def OAI.Ostmann.selectedCompensationCenter line 14
3. theorem OAI.Ostmann.selectedCompensationPrior_nonneg line 17
4. theorem OAI.Ostmann.selectedCompensationPrior_lower line 24

   Source documentation

   This support bound is valid at every index, including unused indices. It therefore supplies the recursive cap without any tail-of-list premise.

   theorem selectedCompensationPrior_lower (A B : Set ℕ) (N : ℕ) (X : ℝ)
       (hi : ℕ) (D P : Finset ℕ) (centers : List ℕ) (n : ℕ) (q : P)
       (hq : selectedCompensationPrior A B N X hi D P centers n q ≠ 0) :
       Real.exp (selectedCompensationCenter centers n - 1) ≤ (q : ℝ) := by
   …

   Mentions: OAI.Ostmann.selectedCompensationPrior, OAI.Ostmann.selectedCompensationCenter

5. theorem OAI.Ostmann.selectedCompensationPrior_properties line 35