log_div_log_pos — Mathlib

English

Generalization of pi-existence: for a finite set of inequivalent absolute values, one can find a that isolates a single index with v_i(a) > 1 and v_j(a) < 1 for j ≠ i.

Русский

Обобщение pi-существования: для конечного множества несопоставимых абсолютных величин можно найти a, который изолирует один индекс с v_i(a) > 1 и v_j(a) < 1 для всех j ≠ i.

LaTeX

$$$ \forall i, \exists a, 1 < v_i(a) \land \forall j \neq i, v_j(a) < 1 $$$

Lean4

theorem log_div_log_pos (h : v.IsEquiv w) {a : F} (ha₀ : a ≠ 0) (ha₁ : w a ≠ 1) : 0 < (w a).log / (v a).log :=
  by
  rcases ha₁.lt_or_gt with hwa | hwa
  ·
    simpa using
      div_pos (neg_pos_of_neg <| log_neg (w.pos ha₀) (hwa)) (neg_pos_of_neg <| log_neg (v.pos ha₀) (h.lt_one_iff.2 hwa))
  · exact div_pos (log_pos <| hwa) (log_pos (h.one_lt_iff.2 hwa))

Похожие утверждения