InitialPrimePrior.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Returning the conditional bulk law to its initial harmonic prior

theorem OAI.Ostmann.initial_prime_prior_bound line 14

Source documentation

Deleting primes after fixing nonbulk coordinates does not change the initial law silently. Its signed mean is controlled by the conditional mean plus the exact restored-mass cost, with the latter's original normalizer.

theorem initial_prime_prior_bound {J : Type*} [Fintype J]
    (P : Finset ℕ) (S D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hnew : ∀ j, 0 < ∑ q ∈ S j \ D j, (q : ℝ)⁻¹)
    (F : (J → P) → ℂ) (B : ℝ) (hF : ∀ x, ‖F x‖ ≤ B) :
    let Z := fun j => (∑ q ∈ S j \ D j, (q : ℝ)⁻¹)⁻¹
…

theorem OAI.Ostmann.initial_prime_prior_deleted_cost line 63

Source documentation

The extra return to the initial law has the same elementary deleted atomic-mass cost; it introduces no new prime-distribution assumption.

theorem initial_prime_prior_deleted_cost {J : Type*} [Fintype J]
    (P : Finset ℕ) (S D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hnew : ∀ j, 0 < ∑ q ∈ S j \ D j, (q : ℝ)⁻¹)
    (F : (J → P) → ℂ) (B H T K : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B)
    (hZ : ∀ j, (∑ q ∈ S j \ D j, (q : ℝ)⁻¹)⁻¹ ≤ Real.exp H)
    (hD : ∀ j, ((D j).card : ℝ) ≤ K)
    (hlow : ∀ j q, q ∈ S j → Real.exp T ≤ (q : ℝ))
    (hsmall : (Fintype.card J : ℝ) * K * Real.exp (H - T) ≤ 1) :
    ‖∑ x, ((∏ j, primeSubsetPrior P (S j) (x j) : ℝ) : ℂ) * F x‖ ≤
      ‖∑ x, ((∏ j, primeSubsetPrior P (S j \ D j) (x j) : ℝ) : ℂ) * F x‖ +
        B * (2 * (Fintype.card J : ℝ) * K * Real.exp (H - T)) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.initial_prime_prior_three_errors line 82

Source documentation

Scalar error assembly is separate from the original observable, avoiding repeated elaboration of its full arithmetic expression.

theorem initial_prime_prior_three_errors {J : Type*} [Fintype J]
    (P : Finset ℕ) (S D : J → Finset ℕ) (hSP : ∀ j, S j ⊆ P)
    (hnew : ∀ j, 0 < ∑ q ∈ S j \ D j, (q : ℝ)⁻¹)
    (F : (J → P) → ℂ) (B main error tail : ℝ) (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 (S j) (x j) : ℝ) : ℂ) * F x‖ ≤
      main + error + 2 * tail := by
…

Mentions: OAI.Ostmann.primeSubsetPrior