MonomialOrder.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326Aux.sign_gap_of_abs_sub_lt line 13
Source documentation
A perturbation by less than half the absolute value preserves the sign and leaves a quantitative gap from zero.
```
theorem sign_gap_of_abs_sub_lt {a b : ℝ}
    (h : |a - b| < |b| / 2) :
    (0 < b → 0 < a ∧ b / 2 < a) ∧
    (b < 0 → a < 0 ∧ a < b / 2) ∧ |b| / 2 < |a| := by
…
```

theorem OAI.Problem326Aux.abs_sum_mul_le line 42

Source documentation

Bounding each coordinate perturbation bounds any finite scalar product.

theorem abs_sum_mul_le {ι : Type uIota} [Fintype ι]
    (p r v : ι → ℝ) (E : ℝ)
    (h : ∀ i, |p i - r i| ≤ E) :
    |∑ i, (p i - r i) * v i| ≤ E * ∑ i, |v i| := by
…

theorem OAI.Problem326Aux.prod_rpow_pow_eq line 55

Source documentation

Monomials at exponential coordinates have the expected scalar exponent.

theorem prod_rpow_pow_eq {ι : Type uIota} [Fintype ι]
    {h : ℝ} (hh : 0 < h) (p : ι → ℝ) (y : ι → ℕ) :
    (∏ i, (h ^ (p i)) ^ (y i)) = h ^ (∑ i, p i * (y i : ℝ)) := by
…

theorem OAI.Problem326Aux.prod_rpow_pow_le_of_gap line 64

Source documentation

An exponent gap orders monomials quantitatively when the base is below one.

theorem prod_rpow_pow_le_of_gap {ι : Type uIota} [Fintype ι]
    {h H : ℝ} (hh : 0 < h) (hh1 : h ≤ 1)
    (p : ι → ℝ) (y z : ι → ℕ)
    (hgap : H ≤ ∑ i, p i * ((z i : ℝ) - (y i : ℝ))) :
    (∏ i, (h ^ (p i)) ^ (z i)) ≤
      h ^ H * (∏ i, (h ^ (p i)) ^ (y i)) := by
…

theorem OAI.Problem326Aux.exists_positive_common_bound line 78

Source documentation

A finite collection of positive thresholds admits a common positive bound, including when the indexing set is empty.

theorem exists_positive_common_bound {ι : Type uIota} (s : Finset ι)
    (f : ι → ℝ) (hf : ∀ i ∈ s, 0 < f i) {C : ℝ} (hC : 0 < C) :
    ∃ E : ℝ, 0 < E ∧ E ≤ C ∧ ∀ i ∈ s, E ≤ f i := by
…

theorem OAI.Problem326Aux.exists_pairing_tolerance line 95

Source documentation

One tolerance controls all nonzero pairings with finitely many directions. No continuity of the eventual tolerance as a function of r is required.

theorem exists_pairing_tolerance {ι : Type uIota} {J : Type uJ} [Fintype ι] [Fintype J]
    (r : ι → ℝ) (v : J → ι → ℝ) :
    ∃ E : ℝ, 0 < E ∧ E ≤ 1 / 2 ∧
      ∀ p : ι → ℝ, (∀ i, |p i - r i| ≤ E) →
      ∀ j, (∑ i, r i * v j i) ≠ 0 →
        |(∑ i, p i * v j i) - (∑ i, r i * v j i)| <
          |∑ i, r i * v j i| / 2 := by
…

theorem OAI.Problem326Aux.exists_positive_pairing_gap line 128

Source documentation

Finite nonzero pairings have a positive common quantitative gap.

theorem exists_positive_pairing_gap {J : Type uJ} [Fintype J] (a : J → ℝ) :
    ∃ H : ℝ, 0 < H ∧ H ≤ 1 ∧ ∀ j, a j ≠ 0 → H ≤ |a j| / 2 := by
…

theorem OAI.Problem326.monomial_rpow line 149

Source documentation

Exact mass-action monomial representation at exponential coordinates.

theorem monomial_rpow {d : ℕ} {h : ℝ} (hh : 0 < h)
    (p : Fin d → ℝ) (y : Fin d → ℕ) :
    monomial (fun i => h ^ p i) y = h ^ (∑ i, p i * (y i : ℝ)) :=
…

Mentions: OAI.Problem326.monomial

theorem OAI.Problem326.monomial_le_rpow_mul_of_gap line 155

Source documentation

Exact monomial-order interface for active-slope sign-gap arguments.

theorem monomial_le_rpow_mul_of_gap {d : ℕ} {h H : ℝ}
    (hh : 0 < h) (hh1 : h ≤ 1) (p : Fin d → ℝ) (y z : Fin d → ℕ)
    (hgap : H ≤ ∑ i, p i * ((z i : ℝ) - (y i : ℝ))) :
    monomial (fun i => h ^ p i) z ≤ h ^ H * monomial (fun i => h ^ p i) y :=
…

Mentions: OAI.Problem326.monomial