OAI/NumberTheory/Ostmann/Construction/TopPrimeSupport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Ostmann.TopPrimeCondition line 11
2. def OAI.Ostmann.TopPrimeCondition.coordinate line 15
3. def OAI.Ostmann.TopPrimeCondition.formula line 19
4. def OAI.Ostmann.TopPrimeCondition.target line 23
5. def OAI.Ostmann.TopPrimeCondition.Holds line 27
6. theorem OAI.Ostmann.TopPrimeCondition.distinct_holds_iff line 30
7. theorem OAI.Ostmann.TopPrimeCondition.formula_value line 35
8. theorem OAI.Ostmann.TopPrimeCondition.formula_cost line 40
9. theorem OAI.Ostmann.TopPrimeCondition.formula_denominator line 43
10. def OAI.Ostmann.TopPrimeCondition.Bounded line 46
11. theorem OAI.Ostmann.TopPrimeCondition.formula_inputs line 50
12. theorem OAI.Ostmann.top_prime_support_bound line 56

    Source documentation

    This bound allows repeated coordinates or a zero external integer. Such conditions have empty support and are covered by the same proved alternative.

    theorem top_prime_support_bound {A J : Type*} [Fintype A] [Nonempty A] [Fintype J] {m : ℕ}
        (prime : A → ℕ) (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
        (checks : J → TopPrimeCondition (Fin (m + 1)))
        (μ : Fin (m + 1) → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a) (hmass : ∀ i, ∑ a, μ i a = 1)
        (α V R : ℝ) (hα : 0 ≤ α) (hV : 0 < V) (hR : 3 ≤ R)
        (hmax : ∀ i a, μ i a ≤ α)
        (hlower : ∀ a, V ≤ Real.log (prime a : ℝ)) (hupper : ∀ a, (prime a : ℝ) ≤ R)
        (hbound : ∀ j, (checks j).Bounded R)
        (W : (Fin (m + 1) → A) → ℂ) (B δ : ℝ)
        (hB : 0 ≤ B) (hδ : 0 ≤ δ) (hW : ∀ x, ‖W x‖ ≤ B)
        (hcancel : ‖∑ x, (productPrior μ x : ℂ) * W x‖ ≤ δ) :
        ‖∑ x, (productPrior μ x : ℂ) *
    …

    Mentions: OAI.Ostmann.TopPrimeCondition, OAI.Ostmann.productPrior