exists_one_lt_lt_one_pi_of_not_isEquiv

English

For a finite family of inequivalent absolute values v_i, there exists a scalar a that makes all but one v_i(a) < 1 while the remaining is ≥ 1, controlled by pairwise inequivalence.

Русский

Для конечной семьи неэквивалентных абсолютных величин v_i существует такое а, чтобы для всех, кроме одной, v_i(a) < 1, а для одной из них выполнено ≥ 1, согласно попарному неэквивалентному отношению.

LaTeX

$$$ \text{Let } v_i \text{ be inequivalent; there exists } a,\ 1 < v_i(a) \text{ and } v_j(a) < 1 \text{ for } j \neq i $$$

Lean4

/-- If `v : ι → AbsoluteValue R S` is a finite collection of non-trivial and pairwise inequivalent
absolute values, then for any `i` there is some `a : R` such that `1 < v i a` and
`v j a < 1` for all `j ≠ i`.
-/
theorem exists_one_lt_lt_one_pi_of_not_isEquiv (h : ∀ i, (v i).IsNontrivial)
    (hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) : ∀ i, ∃ (a : R), 1 < v i a ∧ ∀ j ≠ i, v j a < 1 :=
  by
  let P (ι : Type _) [Fintype ι] : Prop :=
    [DecidableEq ι] →
      ∀ v : ι → AbsoluteValue R S,
        (∀ i, (v i).IsNontrivial) →
          (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) →
            ∀ i,
              ∃ (a : R),
                1 < v i a ∧
                  ∀ j ≠ i,
                    v j a <
                      1
                        -- Use strong induction on the index.

  revert hv h;
  refine induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ _ v h hv i ↦ ?_) (fun ι _ _ ih _ v h hv i ↦ ?_) v
  · -- If `ι` is trivial this follows immediately from `(v i).IsNontrivial`.

    let ⟨a, ha⟩ := (h i).exists_abv_gt_one
    exact ⟨a, ha, fun j hij ↦ absurd (Subsingleton.elim i j) hij.symm⟩
  · rcases eq_or_ne (card ι) 2 with (hc | hc)
    · -- If `ι` has two elements this is `exists_one_lt_lt_one_of_not_isEquiv`.

      let ⟨j, hj⟩ := (Nat.card_eq_two_iff' i).1 <| card_eq_nat_card ▸ hc
      let ⟨a, ha⟩ := (v i).exists_one_lt_lt_one_of_not_isEquiv (h i) (h j) (hv hj.1.symm)
      exact ⟨a, ha.1, fun _ h ↦ hj.2 _ h ▸ ha.2⟩
    have hlt : 2 < card ι := Nat.lt_of_le_of_ne (one_lt_card_iff_nontrivial.2 ‹_›) hc.symm
    let ⟨j, hj⟩ := exists_ne i
    let ⟨a, ha⟩ :=
      ih { k : ι // k ≠ j } (card_subtype_lt fun a ↦ a rfl) (restrict _ v) (fun i ↦ h _)
        (hv.comp_of_injective val_injective)
        ⟨i, hj.symm⟩
          -- Then apply induction next to the subcollection `{v i, v j}` to get `b : K`.

    let ⟨b, hb⟩ :=
      ih { k : ι // k = i ∨ k = j } (by linarith [card_subtype_eq_or_eq_of_ne hj.symm]) (restrict _ v) (fun _ ↦ h _)
        (hv.comp_of_injective val_injective) ⟨i, .inl rfl⟩
    rcases eq_or_ne (v j a) 1 with (ha₁ | ha₁)
    · -- If `v j a = 1` then take a large enough value from the sequence `a ^ n * b`.

      let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_eq_one ha.1 ha.2 ha₁ hb.1 (hb.2 ⟨j, .inr rfl⟩ (by grind))
      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)
    rcases ha₁.lt_or_gt with (ha_lt | ha_gt)
    · -- If `v j a < 1` then `a` works as the divergent point.

      refine ⟨a, ha.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact ha_lt; exact ha.2 ⟨k, h⟩ (by grind)
    · -- If `1 < v j a` then take a large enough value from the sequence `b / (1 + a ^ (-n))`.

      let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_one_lt ha.1 ha.2 ha_gt hb.1 (hb.2 ⟨j, .inr rfl⟩ (by grind))
      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)

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