RepeatedPhysicalPrior.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing repetitions under the original mixed prime priors

theorem OAI.Ostmann.tuple_distinct_weight_exp line 14

Source documentation

Summing the reciprocal weight of the distinct values costs at most n^n, even for tuples which have singleton values.

theorem tuple_distinct_weight_exp {A : Type*} [Fintype A] (n : ℕ)
    (w : A → ℝ) (hw : ∀ a, 0 ≤ w a) :
    (∑ x : Fin n → A, ∏ a ∈ Finset.univ.image x, w a) ≤
      (n : ℝ) ^ n * Real.exp (∑ a, w a) := by
…

theorem OAI.Ostmann.repeated_physical_prior_bound_at line 47

Source documentation

The original smooth/harmonic marginal bounds and the physical repeated- test estimate imply the error in (7.3), retaining every normalizer.

theorem repeated_physical_prior_bound_at {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
    (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
    (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
    (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i)
    (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
    (hmean : ∀ i q, ∑ x, F i q x = 0)
    (henergy : ∀ i (q : P), ∑ x, ‖F i q x‖ ^ 2 ≤ (q : ℝ))
    (ψ : 𝓢(ℝ, ℂ)) (X H R Δ : ℝ) (hX : 0 < X) (hR : 0 < R)
    (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0)
    (E : Finset (Fin n → P)) (hE : ∀ x ∈ E, ¬ Function.Injective x)
    (hsmall : ∀ x ∈ E, ∀ i, H * R < (x i : ℝ))
…

theorem OAI.Ostmann.repeated_physical_prior_bound line 129