Loogle!

Result

Found 9 declarations mentioning Real, HDiv.hDiv, Finset.prod and HPow.hPow.

• Real.harm_mean_le_geom_mean_weighted 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hs : s.Nonempty) (hw : ∀ i ∈ s, 0 < w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 < z i) : (∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
• Real.geom_mean_le_arith_mean 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u_1} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 ≤ z i) : (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹ ≤ (∑ i ∈ s, w i * z i) / ∑ i ∈ s, w i
• Real.harm_mean_le_geom_mean 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) (hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 < z i) : (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹
• integral_sin_pow_even 📋 Mathlib.Analysis.SpecialFunctions.Integrals
  (n : ℕ) : ∫ (x : ℝ) in 0 ..Real.pi, Real.sin x ^ (2 * n) = Real.pi * ∏ i ∈ Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)
• integral_sin_pow_odd 📋 Mathlib.Analysis.SpecialFunctions.Integrals
  (n : ℕ) : ∫ (x : ℝ) in 0 ..Real.pi, Real.sin x ^ (2 * n + 1) = 2 * ∏ i ∈ Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)
• GaussianFourier.integral_cexp_neg_sum_mul_add 📋 Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
  {ι : Type u_2} [Fintype ι] {b : ι → ℂ} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι → ℂ) : ∫ (v : ι → ℝ), Complex.exp (-∑ i, b i * ↑(v i) ^ 2 + ∑ i, c i * ↑(v i)) = ∏ i, (↑Real.pi / b i) ^ (1 / 2) * Complex.exp (c i ^ 2 / (4 * b i))
• MeasureTheory.lintegral_prod_lintegral_pow_le 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i)) [DecidableEq ι] [Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {p : ℝ} (hp : (↑(Fintype.card ι)).HolderConjugate p) {f : ((a : ι) → A a) → ENNReal} (hf : Measurable f) : ∫⁻ (x : (i : ι) → A i), ∏ i, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ (1 / (↑(Fintype.card ι) - 1)) ∂MeasureTheory.Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ p
• Real.tendsto_euler_sin_prod 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  (x : ℝ) : Filter.Tendsto (fun n => Real.pi * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) Filter.atTop (nhds (Real.sin (Real.pi * x)))
• EulerSine.sin_pi_mul_eq 📋 Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
  (z : ℂ) (n : ℕ) : Complex.sin (↑Real.pi * z) = ((↑Real.pi * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ∫ (x : ℝ) in 0 ..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)) / ↑(∫ (x : ℝ) in 0 ..Real.pi / 2, Real.cos x ^ (2 * n))

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 d796b90