NestedPrimePrior.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Returning to an initial law that already excludes prescribed primes

theorem OAI.Ostmann.nested_prime_prior_bound line 13

Source documentation

Global exclusions made when constructing the word remain excluded. Only the extra, nonbulk-dependent deletion is undone. The error can still be charged to the larger shell and its conditional normalizer.

theorem nested_prime_prior_bound {J : Type*} [Fintype J]
    (P : Finset ℕ) (S initial D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hsub : ∀ j, initial j ⊆ S j) (hretain : ∀ j, S j \ D j ⊆ initial j)
    (hnew : ∀ j, 0 < ∑ q ∈ S j \ D j, (q : ℝ)⁻¹)
    (F : (J → P) → ℂ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B) :
    ‖∑ x, ((∏ j, primeSubsetPrior P (initial j) (x j) : ℝ) : ℂ) * F x‖ ≤
      ‖∑ x, ((∏ j, primeSubsetPrior P (S j \ D j) (x j) : ℝ) : ℂ) * F x‖ +
        B * ((∏ j, (1 + (∑ q ∈ S j \ D j, (q : ℝ)⁻¹)⁻¹ *
          ∑ q ∈ S j ∩ D j, (q : ℝ)⁻¹)) - 1) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.nested_prime_prior_three_errors line 53

Source documentation

The initial law may retain any prescribed global exclusions between the full shell and the additionally conditioned law.

theorem nested_prime_prior_three_errors {J : Type*} [Fintype J]
    (P : Finset ℕ) (S initial D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hsub : ∀ j, initial j ⊆ S j) (hretain : ∀ j, S j \ D j ⊆ initial j)
    (hnew : ∀ j, 0 < ∑ q ∈ S j \ D j, (q : ℝ)⁻¹)
    (F : (J → P) → ℂ) (B main error tail : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B)
    (hmean : ‖∑ x, ((∏ j, primeSubsetPrior P (S j \ D j) (x j) : ℝ) : ℂ) * F x‖ ≤
      main + error + tail)
    (herror : B * ((∏ j, (1 + (∑ q ∈ S j \ D j, (q : ℝ)⁻¹)⁻¹ *
      ∑ q ∈ S j ∩ D j, (q : ℝ)⁻¹)) - 1) ≤ tail) :
    ‖∑ x, ((∏ j, primeSubsetPrior P (initial j) (x j) : ℝ) : ℂ) * F x‖ ≤
      main + error + 2 * tail := by
…

Mentions: OAI.Ostmann.primeSubsetPrior