Log le const mul pow
log_le_const_mul_pow
Project documentation
The union of B-sets used in the proof of proposition 2.6. -/ noncomputable def BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ)) := (indexSet' α β γ d x ε).sup fun ⟨r, s, t, c⟩ ↦ B_finset d c (fun i ↦ 2^r i) (fun i ↦ 2^s i) (fun i ↦ 2^t i) theorem similar_pow_log {x : ℕ} (hx : 0 < x) : x ~ 2 ^ Na...
Exact Lean statement
theorem log_le_const_mul_pow {ε : ℝ} (hε : 0 < ε) (d : ℕ) (hd : 0 < d) :
∃ c ≥ 0, ∀ x : ℕ, (Real.log x)^d ≤ c * (x : ℝ)^εFormal artifact
Lean source
theorem log_le_const_mul_pow {ε : ℝ} (hε : 0 < ε) (d : ℕ) (hd : 0 < d) : ∃ c ≥ 0, ∀ x : ℕ, (Real.log x)^d ≤ c * (x : ℝ)^ε := by have := (isLittleO_log_rpow_rpow_atTop d hε).isBigO.natCast_atTop have := this.nat_of_atTop (l := ⊤) ?_ · simp only [Real.rpow_natCast, Asymptotics.isBigO_iff', norm_pow, Real.norm_eq_abs] at this simp only [gt_iff_lt, eventually_top] at this obtain ⟨c, hc_pos, hc⟩ := this refine ⟨c, hc_pos.le, ?_⟩ intro x calc _ ≤ _ := by gcongr exact le_abs_self (Real.log ↑x) _ ≤ _ := hc x _ ≤ _ := by rw [abs_of_nonneg] positivity · simp [Real.rpow_natCast, hε.ne', hd.ne']- Project
- ABC Exceptions
- License
- Apache-2.0
- Commit
- d8ace7bbaa23
- Source
- ABCExceptions/Section2.lean:1439-1456
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Determinant Bound application
DeterminantBound.application
Plain-language statement
A particular application of the determinant bound used in subcase 2.1
Source project: ABC Exceptions
Person-level attribution pending.
Exists nice factorization
exists_nice_factorization
Plain-language statement
Proposition 2.5. The bulk of the proof is in the section NiceFactorization.
Source project: ABC Exceptions
Person-level attribution pending.
Exists nice factorization
exists_nice_factorization'
Plain-language statement
Some basic consequences of Proposition 2.5, phrased in a way that make them more useful in the proof of Proposition 2.6.
Source project: ABC Exceptions
Person-level attribution pending.