Loogle!

Result

Found 1299 declarations mentioning Int.cast. Of these, 22 have a name containing "rpow".

• Real.rpow_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  (x : ℝ) (n : ℤ) : x ^ ↑n = x ^ n
• Real.rpow_intCast_mul 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x : ℝ} (hx : 0 ≤ x) (n : ℤ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z
• Real.rpow_mul_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (n : ℤ) : x ^ (y * ↑n) = (x ^ y) ^ n
• Real.rpow_add_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + ↑n) = x ^ y * x ^ n
• Real.rpow_add_intCast' 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x y : ℝ} (hx : 0 ≤ x) {n : ℤ} (h : y + ↑n ≠ 0) : x ^ (y + ↑n) = x ^ y * x ^ n
• Real.rpow_sub_intCast' 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {x y : ℝ} (hx : 0 ≤ x) {n : ℤ} (h : y - ↑n ≠ 0) : x ^ (y - ↑n) = x ^ y / x ^ n
• ENNReal.rpow_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  (x : ENNReal) (n : ℤ) : x ^ ↑n = x ^ n
• NNReal.rpow_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  (x : NNReal) (n : ℤ) : x ^ ↑n = x ^ n
• ENNReal.rpow_intCast_mul 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  (x : ENNReal) (n : ℤ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z
• ENNReal.rpow_mul_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  (x : ENNReal) (y : ℝ) (n : ℤ) : x ^ (y * ↑n) = (x ^ y) ^ n
• NNReal.rpow_intCast_mul 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  (x : NNReal) (n : ℤ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z
• NNReal.rpow_mul_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  (x : NNReal) (y : ℝ) (n : ℤ) : x ^ (y * ↑n) = (x ^ y) ^ n
• NNReal.rpow_add_intCast 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + ↑n) = x ^ y * x ^ n
• NNReal.rpow_add_intCast' 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {y : ℝ} {n : ℤ} (h : y + ↑n ≠ 0) (x : NNReal) : x ^ (y + ↑n) = x ^ y * x ^ n
• NNReal.rpow_sub_intCast' 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {y : ℝ} {n : ℤ} (h : y - ↑n ≠ 0) (x : NNReal) : x ^ (y - ↑n) = x ^ y / x ^ n
• CFC.rpow_intCast 📋 Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
  {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : Aˣ) (n : ℤ) (ha : 0 ≤ ↑a := by cfc_tac) : ↑a ^ ↑n = ↑(a ^ n)
• Real.summable_abs_int_rpow 📋 Mathlib.Analysis.PSeries
  {b : ℝ} (hb : 1 < b) : Summable fun n => |↑n| ^ (-b)
• Real.summable_one_div_int_add_rpow 📋 Mathlib.Analysis.PSeries
  (a s : ℝ) : (Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s
• Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (hFf : Real.fourierIntegral f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), Real.fourierIntegral f ↑n * (fourier n) ↑x
• Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay_of_summable 📋 Mathlib.Analysis.Fourier.PoissonSummation
  {f : ℝ → ℂ} (hc : Continuous f) {b : ℝ} (hb : 1 < b) (hf : f =O[Filter.cocompact ℝ] fun x => |x| ^ (-b)) (hFf : Summable fun n => Real.fourierIntegral f ↑n) (x : ℝ) : ∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), Real.fourierIntegral f ↑n * (fourier n) ↑x
• NumberField.abs_discr_rpow_ge_of_isTotallyComplex 📋 Mathlib.NumberTheory.NumberField.Discriminant.Basic
  (K : Type u_1) [Field K] [NumberField K] [NumberField.IsTotallyComplex K] : ↑(Module.finrank ℚ K) ^ 2 / (4 / Real.pi * ↑(Module.finrank ℚ K).factorial ^ (2 * (↑(Module.finrank ℚ K))⁻¹)) ≤ ↑|NumberField.discr K| ^ (↑(Module.finrank ℚ K))⁻¹
• LiouvilleWith.frequently_lt_rpow_neg 📋 Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
  {p q x : ℝ} (h : LiouvilleWith p x) (hlt : q < p) : ∃ᶠ (n : ℕ) in Filter.atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision e0654b0