Positive rational exponent scales -- proof internals

theorem Complexity.PositiveRationalScale.instNonempty : Nonempty PositiveRationalScale

theorem Complexity.PositiveRationalScale.instIsCodirectedOrder : IsCodirectedOrder PositiveRationalScale

theorem Complexity.PositiveRationalScale.value_pos_internal (scale : PositiveRationalScale) : 0 < scale.value

theorem Complexity.PositiveRationalScale.eventually_atZeroFromPositive_iff_internal {predicate : PositiveRationalScale → Prop} : (∀ᶠ (scale : PositiveRationalScale) in atZeroFromPositive, predicate scale) ↔ ∃ (cutoff : PositiveRationalScale), ∀ scale ≤ cutoff, predicate scale

theorem Complexity.PositiveRationalScale.floorMul_zero_internal (scale : PositiveRationalScale) : scale.floorMul 0 = 0

theorem Complexity.PositiveRationalScale.ceilMul_zero_internal (scale : PositiveRationalScale) : scale.ceilMul 0 = 0

theorem Complexity.PositiveRationalScale.floorMul_mono_internal (scale : PositiveRationalScale) : Monotone scale.floorMul

theorem Complexity.PositiveRationalScale.floorMul_add_le_internal (scale : PositiveRationalScale) (first second : ℕ) : scale.floorMul first + scale.floorMul second ≤ scale.floorMul (first + second)

theorem Complexity.PositiveRationalScale.tendsto_floorMul_atTop_internal (scale : PositiveRationalScale) : Filter.Tendsto scale.floorMul Filter.atTop Filter.atTop

theorem Complexity.PositiveRationalScale.eventually_coefficient_mul_succ_le_two_pow_internal (coefficient : ℕ) : ∀ᶠ (exponent : ℕ) in Filter.atTop, coefficient * (exponent + 1) ≤ 2 ^ exponent

theorem Complexity.PositiveRationalScale.eventually_coefficient_mul_succ_pow_le_two_pow_internal (coefficient degree : ℕ) : ∀ᶠ (exponent : ℕ) in Filter.atTop, coefficient * (exponent + 1) ^ degree ≤ 2 ^ exponent

theorem Complexity.PositiveRationalScale.eventually_coefficient_mul_succ_pow_le_powFloor_internal (scale : PositiveRationalScale) (coefficient degree : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, coefficient * (n + 1) ^ degree ≤ scale.powFloor n

theorem Complexity.PositiveRationalScale.ceilMul_mono_internal (scale : PositiveRationalScale) : Monotone scale.ceilMul

theorem Complexity.PositiveRationalScale.denominator_mul_floorMul_le_internal (scale : PositiveRationalScale) (n : ℕ) : scale.denominator * scale.floorMul n ≤ scale.numerator * n

theorem Complexity.PositiveRationalScale.numerator_mul_le_denominator_mul_ceilMul_internal (scale : PositiveRationalScale) (n : ℕ) : scale.numerator * n ≤ scale.denominator * scale.ceilMul n

theorem Complexity.PositiveRationalScale.floorMul_le_ceilMul_internal (scale : PositiveRationalScale) (n : ℕ) : scale.floorMul n ≤ scale.ceilMul n

theorem Complexity.PositiveRationalScale.ceilMul_le_floorMul_add_one_internal (scale : PositiveRationalScale) (n : ℕ) : scale.ceilMul n ≤ scale.floorMul n + 1

theorem Complexity.PositiveRationalScale.floorMul_pos_of_denominator_le_numerator_mul_internal (scale : PositiveRationalScale) {n : ℕ} (hlarge : scale.denominator ≤ scale.numerator * n) : 0 < scale.floorMul n

theorem Complexity.PositiveRationalScale.powFloor_pos_internal (scale : PositiveRationalScale) (n : ℕ) : 0 < scale.powFloor n

theorem Complexity.PositiveRationalScale.powCeil_pos_internal (scale : PositiveRationalScale) (n : ℕ) : 0 < scale.powCeil n

theorem Complexity.PositiveRationalScale.powFloor_mono_internal (scale : PositiveRationalScale) : Monotone scale.powFloor

theorem Complexity.PositiveRationalScale.powFloor_mul_le_powFloor_add_internal (scale : PositiveRationalScale) (first second : ℕ) : scale.powFloor first * scale.powFloor second ≤ scale.powFloor (first + second)

theorem Complexity.PositiveRationalScale.powFloor_pow_le_mul_internal (scale : PositiveRationalScale) (n multiplier : ℕ) : scale.powFloor n ^ multiplier ≤ scale.powFloor (multiplier * n)

theorem Complexity.PositiveRationalScale.powCeil_mono_internal (scale : PositiveRationalScale) : Monotone scale.powCeil

theorem Complexity.PositiveRationalScale.powFloor_le_powCeil_internal (scale : PositiveRationalScale) (n : ℕ) : scale.powFloor n ≤ scale.powCeil n

theorem Complexity.PositiveRationalScale.powCeil_le_two_mul_powFloor_internal (scale : PositiveRationalScale) (n : ℕ) : scale.powCeil n ≤ 2 * scale.powFloor n

theorem Complexity.PositiveRationalScale.onePlusCeilPow_eq_mul_internal (scale : PositiveRationalScale) (n : ℕ) : scale.onePlusCeilPow n = 2 ^ n * scale.powCeil n

theorem Complexity.PositiveRationalScale.two_pow_le_onePlusCeilPow_internal (scale : PositiveRationalScale) (n : ℕ) : 2 ^ n ≤ scale.onePlusCeilPow n

theorem Complexity.PositiveRationalScale.onePlusCeilPowAtLength_pow_internal (scale : PositiveRationalScale) (n : ℕ) : scale.onePlusCeilPowAtLength (2 ^ n) = scale.onePlusCeilPow n