SignTolerance.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.exists_sign_tolerance line 14

Source comment

The existence form avoids imposing any continuity on the chosen tolerance.

theorem exists_sign_tolerance {d : ℕ} (D : Finset (Fin d → ℝ))
    (r : Fin d → ℝ) :
    ∃ E : ℝ, 0 < E ∧ E ≤ 1 / 2 ∧
      ∀ p : Fin d → ℝ, (∀ i, |p i - r i| < E) →
        ∀ v ∈ D, (∑ i, r i * v i) ≠ 0 →
          |(∑ i, p i * v i) - (∑ i, r i * v i)| <
            |∑ i, r i * v i| / 2 := by
…

theorem OAI.Problem326.sign_and_half_gap_of_abs_sub_lt line 49

Source documentation

A perturbation smaller than half a nonzero value preserves its sign and half-gap.

theorem sign_and_half_gap_of_abs_sub_lt {p r : ℝ} (hr : r ≠ 0)
    (hclose : |p - r| < |r| / 2) :
    (0 < p ↔ 0 < r) ∧ (p < 0 ↔ r < 0) ∧ |r| / 2 < |p| := by
…

theorem OAI.Problem326.finite_positive_lower_bound line 69

Source documentation

Any finite family of positive real numbers has a common positive lower bound.

theorem finite_positive_lower_bound {α : Type uAlpha} (S : Finset α) (f : α → ℝ)
    (hf : ∀ a ∈ S, 0 < f a) :
    ∃ H : ℝ, 0 < H ∧ H ≤ 1 ∧ ∀ a ∈ S, H ≤ f a := by
…

theorem OAI.Problem326.exists_uniform_dot_gap line 85

Source documentation

In a fixed finite slope family, all nonzero comparisons have a uniform half-gap.

theorem exists_uniform_dot_gap {d : ℕ} (R D : Finset (Fin d → ℝ)) :
    ∃ H : ℝ, 0 < H ∧ H ≤ 1 ∧
      ∀ r ∈ R, ∀ v ∈ D, (∑ i, r i * v i) ≠ 0 →
        H ≤ |∑ i, r i * v i| / 2 := by
…

theorem OAI.Problem326.exists_sign_tolerance_function line 100

Source documentation

The tolerance can be selected pointwise; no regularity of it is required.

theorem exists_sign_tolerance_function {d : ℕ} (D : Finset (Fin d → ℝ)) :
    ∃ E : (Fin d → ℝ) → ℝ,
      (∀ r, 0 < E r ∧ E r ≤ 1 / 2) ∧
      ∀ r p : Fin d → ℝ, (∀ i, |p i - r i| < E r) →
        ∀ v ∈ D, (∑ i, r i * v i) ≠ 0 →
          (0 < (∑ i, p i * v i) ↔ 0 < (∑ i, r i * v i)) ∧
          ((∑ i, p i * v i) < 0 ↔ (∑ i, r i * v i) < 0) ∧
          |∑ i, r i * v i| / 2 < |∑ i, p i * v i| := by
…