FormalConjecturesForMathlib/Analysis/SpecialFunctions/Log/Basic.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def Real.iteratedLog The iterated logarithm of x is the number of times the natural logarithm must be iteratively applied before the result is less than or equal to 1 line 30 source

   Source documentation

   The iterated logarithm of x is the number of times the natural logarithm must be iteratively applied before the result is less than or equal to 1. Reference: https://en.wikipedia.org/wiki/Iterated_logarithm

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

   Statement uses: Real, Nat

   Proof uses: InfSet.sInf, Set.ofPred, Real.iteratedLog.match_1, LE.le, Nat.iterate, Real.log, OfNat.ofNat

   4 instances, coercions and auxiliary constants left out.

   noncomputable def Real.iteratedLog (x : ℝ) : ℕ :=
   …

2. def Nat.iteratedLog The iterated logarithm of a natural number in base b: the number of times Nat.log b must be iteratively applied to n before the result is at most 1 line 35 source

   Source documentation

   The iterated logarithm of a natural number in base b: the number of times Nat.log b must be iteratively applied to n before the result is at most 1.

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

   Statement uses: Nat

   Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, Nat.iteratedLog.match_1, Unit, OfNat.ofNat, Nat.succ, HAdd.hAdd, Nat.log

   5 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

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

   def Nat.iteratedLog (b : ℕ) : ℕ → ℕ
     | 0 => 0
     | 1 => 0
     | (n + 2) => Nat.iteratedLog b (Nat.log b (n + 2)) + 1
   termination_by n => n
   decreasing_by exact Nat.log_lt_self b (by omega)
   
   @[simp]

3. theorem Nat.iteratedLog_zero line 43 source

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

   Statement uses: Nat, Eq, Nat.iteratedLog, OfNat.ofNat

   Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.iteratedLog.eq_1, eq_self

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

4. theorem Nat.iteratedLog_one line 47 source

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

   Statement uses: Nat, Eq, Nat.iteratedLog, OfNat.ofNat

   Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.iteratedLog.eq_2, eq_self

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

5. theorem Nat.iteratedLog_of_two_le line 50 source

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

   Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Nat.iteratedLog, HAdd.hAdd, Nat.log

   Proof uses: Exists, Exists.intro, HSub.hSub, Decidable.byContradiction, Not, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.iteratedLog.eq_3, eq_self, Eq.symm

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 3 steps

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

6. theorem Real.iteratedLog_eq_zero_of_le line 55 source

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

   Statement uses: Real, LE.le, OfNat.ofNat, Eq, Nat, Real.iteratedLog

   Proof uses: Eq.mpr, Or, Set, Set.ofPred, Nat.iterate, Real.log, EmptyCollection.emptyCollection, id, Or.inl

   10 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

7. theorem Real.iteratedLog_eq_zero_of_neg line 59 source

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

   Statement uses: Real, LT.lt, OfNat.ofNat, Eq, Nat, Real.iteratedLog

   Proof uses: Real.iteratedLog_eq_zero_of_le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 32 more

   56 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

8. theorem iteratedLog_two line 63 source

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

   Statement uses: Eq, Nat, Real.iteratedLog, OfNat.ofNat, Real

   Proof uses: id, LE.le, Real.log, Eq.mpr, HSub.hSub, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_sub, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.instAtLeastTwo, Int and 28 more

   44 instances, coercions and auxiliary constants left out.

   Tactic trace: 8 steps

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

9. theorem iteratedLog_four line 71 source

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

   Statement uses: Eq, Nat, Real.iteratedLog, OfNat.ofNat, Real

   Proof uses: id, LE.le, Nat.iterate, Real.log, Ne, Real.sqrt, Eq.mpr, Not, Neg.neg, congrArg, Eq.trans, Or, False, congr, of_eq_true, congrFun', false_or, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 142 more

   141 instances, coercions and auxiliary constants left out.

   Tactic trace: 26 steps

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