FLT/Mathlib/Topology/Algebra/Order/Field.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem AbsoluteValue.lt_one_iff_of_lt_one_imp If v is a nontrivial absolute value, and w is another absolute value such that w x < 1 if v x < 1, then we must also have v x < 1 if w x < 1 line 31 source

   Source documentation

   If v is a nontrivial absolute value, and w is another absolute value such that w x < 1 if v x < 1, then we must also have v x < 1 if w x < 1.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, LinearOrder, IsStrictOrderedRing, AbsoluteValue, Archimedean, TopologicalSpace, OrderTopology, AbsoluteValue.IsNontrivial, LT.lt, OfNat.ofNat, Iff

   Proof uses: Exists, And, Ne, AbsoluteValue.IsNontrivial.exists_abv_lt_one, Iff.intro, Decidable.byContradiction, Not, Nat, HPow.hPow, HMul.hMul, HDiv.hDiv, Eq.mpr, id, Eq, congrArg, propext, AbsoluteValue.mul_one_div_pow_lt_iff, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl and 75 more

   100 instances, coercions and auxiliary constants left out.

   Tactic trace: 19 steps

   Open to load the checked before-and-after goal states.

   theorem lt_one_iff_of_lt_one_imp [Archimedean S] [TopologicalSpace S] [OrderTopology S]
         (hv : v.IsNontrivial) (h : ∀ x, v x < 1 → w x < 1) {a : F} :
       v a < 1 ↔ w a < 1:= by
   …

2. theorem AbsoluteValue.log_div_image_eq_singleton_of_le_one_iff If v and w are two real absolute values on F, v is non-trivial, and v x < 1 if and only if w x < 1, then log (v a) / log (w a) is constant for all a ∈ K line 57 source

   Source documentation

   If v and w are two real absolute values on F, v is non-trivial, and v x < 1 if and only if w x < 1, then log (v a) / log (w a) is constant for all a ∈ K.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AbsoluteValue, Real, AbsoluteValue.IsNontrivial, Iff, LT.lt, OfNat.ofNat, HDiv.hDiv, Real.log, Exists, Eq

   Proof uses: AbsoluteValue.IsNontrivial.exists_abv_gt_one, Exists.intro, Decidable.byContradiction, Not, Classical.byCases, False, Ne, Iff.mp, AbsoluteValue.one_lt_iff_of_lt_one_iff, Eq.mpr, HMul.hMul, id, congrArg, propext, div_lt_div_iff₀, Real.log_pos, mul_comm, Eq.symm, Rat, And and 78 more

   136 instances, coercions and auxiliary constants left out.

   Tactic trace: 33 steps

   Open to load the checked before-and-after goal states.

   theorem log_div_image_eq_singleton_of_le_one_iff {v w : AbsoluteValue F ℝ}
       (hv : v.IsNontrivial)
       (h : ∀ x, v x < 1 ↔ w x < 1) :
       let f : F → ℝ := fun a => Real.log (v a) / Real.log (w a)
   …

3. theorem AbsoluteValue.exists_rpow_of_one_lt line 92 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AbsoluteValue, Real, AbsoluteValue.IsNontrivial, Iff, LT.lt, OfNat.ofNat, Exists, Eq, HPow.hPow

   Proof uses: HDiv.hDiv, Real.log, AbsoluteValue.log_div_image_eq_singleton_of_le_one_iff, Exists.intro, div_pos, Real.log_pos, Iff.mp, AbsoluteValue.one_lt_iff_of_lt_one_iff, Eq.mpr, id, congrArg, Eq.symm, HMul.hMul, Inv.inv, div_eq_inv_mul, Real.rpow_mul, AbsoluteValue.nonneg, Real.exp, Real.rpow_inv_log, lt_of_not_ge and 54 more

   104 instances, coercions and auxiliary constants left out.

   Tactic trace: 8 steps

   Open to load the checked before-and-after goal states.

4. theorem AbsoluteValue.eq_rpow_iff_lt_one_iff Let v and w be two real absolute values on F, where v is non-trivial line 109 source

   Source documentation

   Let v and w be two real absolute values on F, where v is non-trivial. The condition that v x < 1 if and only if w x < 1 is equivalent to the condition that v = w ^ t for some real t > 0.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AbsoluteValue, Real, AbsoluteValue.IsNontrivial, Iff, Exists, LT.lt, OfNat.ofNat, Eq, HPow.hPow

   Proof uses: Iff.intro, Eq.rec, Real.rpow_lt_one_iff', AbsoluteValue.nonneg, Eq.symm, GT.gt, AbsoluteValue.exists_rpow_of_one_lt, Exists.intro, dite, Eq.mpr, id, congrArg, Iff.mp, map_eq_zero, map_zero, Real.zero_rpow, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd and 59 more

   110 instances, coercions and auxiliary constants left out.

   Tactic trace: 21 steps

   Open to load the checked before-and-after goal states.

   theorem eq_rpow_iff_lt_one_iff {v : AbsoluteValue F ℝ} (w : AbsoluteValue F ℝ)
       (hv : v.IsNontrivial) :
       (∃ (t : ℝ) (_ : 0 < t), ∀ x, v x = (w x) ^ t) ↔ (∀ x, v x < 1 ↔ w x < 1) := by
   …

5. theorem AbsoluteValue.exists_lt_one_one_le_of_ne_rpow If v is non-trivial and v = w ^ t for some t > 0, then we can find an a ∈ F such that v a < 1 while 1 ≤ w a line 133 source

   Source documentation

   If v is non-trivial and v = w ^ t for some t > 0, then we can find an a ∈ F such that v a < 1 while 1 ≤ w a.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AbsoluteValue, Real, AbsoluteValue.IsNontrivial, Not, Exists, LT.lt, OfNat.ofNat, Eq, HPow.hPow, And, LE.le

   Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, id, implies_congr, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, Eq.refl, Iff.mpr, Iff, AbsoluteValue.eq_rpow_iff_lt_one_iff, AbsoluteValue.lt_one_iff_of_lt_one_imp

   44 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.

   theorem exists_lt_one_one_le_of_ne_rpow {v w : AbsoluteValue F ℝ}
       (hv : v.IsNontrivial)
       (h : ¬∃ (t : ℝ) (_ : 0 < t), ∀ x, v x = (w x) ^ t) :
       ∃ a : F, v a < 1 ∧ 1 ≤ w a := by
   …

6. theorem AbsoluteValue.ne_pow_symm line 140 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AbsoluteValue, Real, Not, Exists, LT.lt, OfNat.ofNat, Eq, HPow.hPow

   Proof uses: Eq.mpr, id, Eq.trans, And, congrArg, funext, forall_congr, implies_congr, Eq.refl, Inv.inv, Eq.mp, Iff.mpr, inv_pos, Exists.intro, Mathlib.Tactic.Contrapose.contrapose₄, Real.eq_rpow_inv, AbsoluteValue.nonneg, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, HAdd.hAdd and 38 more

   84 instances, coercions and auxiliary constants left out.

   Tactic trace: 5 steps

   Open to load the checked before-and-after goal states.

7. theorem AbsoluteValue.exists_one_lt_lt_one_of_ne_rpow If v and w are two non-trivial absolute values such that v = w ^ t for some t > 0, then we can find an a ∈ K such that 1 < v a while w a < 1 line 151 source

   Source documentation

   If v and w are two non-trivial absolute values such that v = w ^ t for some t > 0, then we can find an a ∈ K such that 1 < v a while w a < 1.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AbsoluteValue, Real, AbsoluteValue.IsNontrivial, Not, Exists, LT.lt, OfNat.ofNat, Eq, HPow.hPow, And

   Proof uses: LE.le, AbsoluteValue.exists_lt_one_one_le_of_ne_rpow, AbsoluteValue.ne_pow_symm, Exists.intro, HDiv.hDiv, Eq.mpr, id, congr, congrArg, map_div₀, congrFun', And.intro, Iff.mpr, one_lt_div, AbsoluteValue.pos_of_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg and 49 more

   95 instances, coercions and auxiliary constants left out.

   Tactic trace: 9 steps

   Open to load the checked before-and-after goal states.

   theorem exists_one_lt_lt_one_of_ne_rpow {v w : AbsoluteValue F ℝ}
       (hv : v.IsNontrivial)
       (hw : w.IsNontrivial)
       (h : ¬∃ (t : ℝ) (_ : 0 < t), ∀ x, v x = (w x) ^ t) :
       ∃ a : F, 1 < v a ∧ w a < 1 := by
   …