SymbolicLineComparison.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Signed replacement of accidental arithmetic flags

After denominators are cleared in §8, coefficient and minor tests are integer polynomials. Under independent representative priors, replacing their congruence flags by their rational polynomial-identity flags has the following quantitative error. The polynomial root and prime-divisor estimates are proved inputs here.

def OAI.Ostmann.arithmeticTestFlag line 19
Source documentation
Use one fixed decision procedure in statements and proofs.
```
noncomputable def arithmeticTestFlag (P : Prop) : Bool := by
…
```
theorem OAI.Ostmann.arithmeticTestFlag_of_true line 23
theorem OAI.Ostmann.arithmeticTestFlag_of_false line 26
theorem OAI.Ostmann.arithmeticTestFlag_eq_true_iff line 29
theorem OAI.Ostmann.arithmeticTestFlag_eq_false_iff line 34

theorem OAI.Ostmann.polynomial_flags_agree line 41

Source documentation

The actual divisibility flags agree with the symbolic identity flags away from the accidental zeros of nonzero polynomials.

theorem polynomial_flags_agree {X I : Type*} {n : ℕ}
    (F : I → MvPolynomial (Fin n) ℚ) (value : X → Fin n → ℚ)
    (N : I → X → ℕ)
    (hzero : ∀ i x, N i x = 0 ↔ MvPolynomial.eval (value x) (F i) = 0)
    (x : X) (p : ℕ) (hgood : ∀ i, ¬(F i ≠ 0 ∧ p ∣ N i x)) :
    (fun i => arithmeticTestFlag (p ∣ N i x)) = (fun i => arithmeticTestFlag (F i = 0)) := by
…

Mentions: OAI.Ostmann.arithmeticTestFlag

theorem OAI.Ostmann.weighted_prime_event_sum line 55
theorem OAI.Ostmann.polynomial_event_bound line 69

theorem OAI.Ostmann.polynomial_symbolic_comparison_le line 95

Source documentation

Signed comparison for any bounded amplitude depending on the coefficient and minor flags, with the smooth and spectator variables left untouched.

theorem polynomial_symbolic_comparison_le {A I : Type*} [Fintype A] [Fintype I]
    {n : ℕ} (value : A → ℚ) (hinj : Function.Injective value)
    (F : I → MvPolynomial (Fin n) ℚ)
    (μ : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
    (hmass : ∀ i, ∑ a, μ i a = 1)
    (α : ℝ) (hα : 0 ≤ α) (hmax : ∀ i a, μ i a ≤ α)
    (P : Finset ℕ) (ν : ℕ → ℝ) (hν : ∀ p ∈ P, 0 ≤ ν p)
    (hνmass : ∑ p ∈ P, ν p = 1)
    (N : I → (Fin n → A) → ℕ)
    (hzero : ∀ i x, N i x = 0 ↔ MvPolynomial.eval (fun j => value (x j)) (F i) = 0)
    (β K : ℝ) (hβ : 0 ≤ β) (hK : 0 ≤ K) (hνmax : ∀ p ∈ P, ν p ≤ β)
    (hcard : ∀ i x, N i x ≠ 0 → ((P.filter fun p => p ∣ N i x).card : ℝ) ≤ K)
…