Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.Table4Ext.eval_expSplitNegXpow_eq_xpow

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row11 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row11.lean:212 to 225

Source documentation

expSplitNegXpow n evaluated at s = √(log x) is exactly x^{-1/n} (for x > 0, log x ≥ 0).

Exact Lean statement

lemma eval_expSplitNegXpow_eq_xpow (n : ℕ) (hn : 0 < n) (x : ℝ)
    (hxpos : 0 < x) (hL : 0 ≤ Real.log x) :
    Expr.eval (fun _ => Real.sqrt (Real.log x)) (expSplitNegXpow n) = x ^ (-(1:ℝ)/n)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eval_expSplitNegXpow_eq_xpow (n : ℕ) (hn : 0 < n) (x : ℝ)    (hxpos : 0 < x) (hL : 0 ≤ Real.log x) :    Expr.eval (fun _ => Real.sqrt (Real.log x)) (expSplitNegXpow n) = x ^ (-(1:ℝ)/n) := by  have hnpos : (0:ℝ) < (n:ℝ) := by exact_mod_cast hn  have hnne : (n:ℝ) ≠ 0 := ne_of_gt hnpos  have hss : Real.sqrt (Real.log x) * Real.sqrt (Real.log x) = Real.log x :=    Real.mul_self_sqrt hL  simp only [expSplitNegXpow, eval_sqE, Expr.eval_exp, Expr.eval_mul, Expr.eval_const,    Expr.eval_var, ← pow_mul]  rw [← Real.exp_nat_mul, hss, Real.rpow_def_of_pos hxpos]  congr 1  simp only [xpowCoef]  push_cast  field_simp