Loogle!

Result

Found 57 declarations mentioning Real, Finset.prod and HPow.hPow.

• Real.rpow_sum_of_pos 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {ι : Type u_1} {a : ℝ} (ha : 0 < a) (f : ι → ℝ) (s : Finset ι) : a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
• Real.rpow_sum_of_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Pow.Real
  {ι : Type u_1} {a : ℝ} (ha : 0 ≤ a) {s : Finset ι} {f : ι → ℝ} (h : ∀ x ∈ s, 0 ≤ f x) : a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
• NNReal.finset_prod_rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ) : ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
• ENNReal.prod_coe_rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ) : ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r
• ENNReal.prod_rpow_of_nonneg 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} {r : ℝ} (hr : 0 ≤ r) : ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
• ENNReal.prod_rpow_of_ne_top 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} (hf : ∀ i ∈ s, f i ≠ ⊤) (r : ℝ) : ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
• Real.finset_prod_rpow 📋 Mathlib.Analysis.SpecialFunctions.Pow.NNReal
  {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) (hs : ∀ i ∈ s, 0 ≤ f i) (r : ℝ) : ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
• NNReal.geom_mean_le_arith_mean_weighted 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → NNReal) (hw' : ∑ i ∈ s, w i = 1) : ∏ i ∈ s, z i ^ ↑(w i) ≤ ∑ i ∈ s, w i * z i
• Real.geom_mean_le_arith_mean_weighted 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
• Real.geom_mean_weighted_of_constant 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : ∏ i ∈ s, z i ^ w i = x
• 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_eq_arith_mean_weighted_of_constant 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
• Real.geom_mean_eq_arith_mean_weighted_iff' 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
• Real.geom_mean_lt_arith_mean_weighted_iff_of_pos 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
• 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.geom_mean_eq_arith_mean_weighted_iff 📋 Mathlib.Analysis.MeanInequalities
  {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z 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)⁻¹
• ENNReal.lintegral_prod_norm_pow_le 📋 Mathlib.MeasureTheory.Integral.MeanInequalities
  {α : Type u_2} {ι : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι) {f : ι → α → ENNReal} (hf : ∀ i ∈ s, AEMeasurable (f i) μ) {p : ι → ℝ} (hp : ∑ i ∈ s, p i = 1) (h2p : ∀ i ∈ s, 0 ≤ p i) : ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
• ENNReal.lintegral_mul_prod_norm_pow_le 📋 Mathlib.MeasureTheory.Integral.MeanInequalities
  {α : Type u_2} {ι : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι) {g : α → ENNReal} {f : ι → α → ENNReal} (hg : AEMeasurable g μ) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) (q : ℝ) {p : ι → ℝ} (hpq : q + ∑ i ∈ s, p i = 1) (hq : 0 ≤ q) (hp : ∀ i ∈ s, 0 ≤ p i) : ∫⁻ (a : α), g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤ (∫⁻ (a : α), g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
• MultilinearMap.restr_norm_le 📋 Mathlib.Analysis.NormedSpace.Multilinear.Basic
  {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [SeminormedAddCommGroup G'] [NormedSpace 𝕜 G'] {k n : ℕ} (f : MultilinearMap 𝕜 (fun x => G) G') (s : Finset (Fin n)) (hk : s.card = k) (z : G) {C : ℝ} (H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖) (v : Fin k → G) : ‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i, ‖v i‖
• MultilinearMap.norm_image_sub_le_of_bound 📋 Mathlib.Analysis.NormedSpace.Multilinear.Basic
  {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [NontriviallyNormedField 𝕜] [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (f : MultilinearMap 𝕜 E G) {C : ℝ} (hC : 0 ≤ C) (H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : (i : ι) → E i) : ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
• FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1 📋 Mathlib.Analysis.Analytic.Inverse
  (n : ℕ) (p : ℕ → ℝ) (hp : ∀ (k : ℕ), 0 ≤ p k) {r a : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a) : ∑ k ∈ Finset.Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, p (c.blocksFun j) ≤ ∑ j ∈ Finset.Ico 2 (n + 1), r ^ j * (∑ k ∈ Finset.Ico 1 n, a ^ k * p k) ^ j
• 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)
• VectorFourier.fourierPowSMulRight_apply 📋 Mathlib.Analysis.Fourier.FourierTransformDeriv
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} {v : V} {n : ℕ} {m : Fin n → W} : (VectorFourier.fourierPowSMulRight L f v n) m = (-(2 * ↑Real.pi * Complex.I)) ^ n • (∏ i, (L v) (m i)) • f v
• MeasureTheory.integral_fintype_prod_eq_pow 📋 Mathlib.MeasureTheory.Integral.Pi
  {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} (ι : Type u_3) [Fintype ι] (f : E → 𝕜) [MeasureTheory.MeasureSpace E] [MeasureTheory.SigmaFinite MeasureTheory.volume] : ∫ (x : ι → E), ∏ i, f (x i) = (∫ (x : E), f x) ^ Fintype.card ι
• 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.GridLines.T_univ 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i)) [DecidableEq ι] {p : ℝ} [Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (f : ((i : ι) → A i) → ENNReal) (x : (i : ι) → A i) : MeasureTheory.GridLines.T μ p f Finset.univ x = ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑(Fintype.card ι) - 1) * p) * ∏ i, (∫⁻ (t : A i), f (Function.update x i t) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ
• 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
• MeasureTheory.GridLines.T.eq_1 📋 Mathlib.Analysis.FunctionalSpaces.SobolevInequality
  {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i)) [DecidableEq ι] (p : ℝ) (f : ((i : ι) → A i) → ENNReal) (s : Finset ι) : MeasureTheory.GridLines.T μ p f s = ∫⋯∫⁻_s, f ^ (1 - (↑s.card - 1) * p) * ∏ i ∈ s, (∫⋯∫⁻_{i}, f ∂μ) ^ p ∂μ
• MeasureTheory.lintegral_mul_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₀ : 0 ≤ p) (hp : (↑(Fintype.card ι) - 1) * p ≤ 1) {f : ((i : ι) → A i) → ENNReal} (hf : Measurable f) : ∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑(Fintype.card ι) - 1) * p) * ∏ i, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ (1 + 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))
• norm_torusIntegral_le_of_norm_le_const 📋 Mathlib.MeasureTheory.Integral.TorusIntegral
  {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : (Fin n → ℂ) → E} {c : Fin n → ℂ} {R : Fin n → ℝ} {C : ℝ} (hf : ∀ (θ : Fin n → ℝ), ‖f (torusMap c R θ)‖ ≤ C) : ‖∯ (x : Fin n → ℂ) in T(c, R), f x‖ ≤ ((2 * Real.pi) ^ n * ∏ i, |R i|) * C
• NumberField.InfinitePlace.prod_eq_abs_norm 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
  {K : Type u_2} [Field K] [NumberField K] (x : K) : ∏ w, w x ^ w.mult = ↑|(Algebra.norm ℚ) x|
• NumberField.mixedEmbedding.norm_apply 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
  {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K) : NumberField.mixedEmbedding.norm x = ∏ w, (NumberField.mixedEmbedding.normAtPlace w) x ^ w.mult
• NumberField.mixedEmbedding.norm.eq_1 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
  {K : Type u_1} [Field K] [NumberField K] : NumberField.mixedEmbedding.norm = { toFun := fun x => ∏ w, (NumberField.mixedEmbedding.normAtPlace w) x ^ w.mult, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
• NumberField.mixedEmbedding.convexBodyLT_volume 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
  (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) [NumberField K] : MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) = ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)
• NumberField.mixedEmbedding.convexBodyLT'_volume 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
  (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w // w.IsComplex }) [NumberField K] : MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀) = ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑(∏ w, f w ^ w.mult)
• EulerProduct.prod_primesBelow_tsum_eq_tsum_smoothNumbers 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun x => ‖f x‖) (N : ℕ) : ∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑N.smoothNumbers), f ↑m
• EulerProduct.prod_filter_prime_tsum_eq_tsum_factoredNumbers 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun x => ‖f x‖) (s : Finset ℕ) : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∑' (m : ↑(Nat.factoredNumbers s)), f ↑m
• EulerProduct.eulerProduct 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : Summable fun x => ‖f x‖) (hf₀ : f 0 = 0) : Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ℕ), f n))
• EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖) (N : ℕ) : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))
• EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {R : Type u_1} [NormedCommRing R] {f : ℕ → R} [CompleteSpace R] (hf₁ : f 1 = 1) (hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n) (hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖) (s : Finset ℕ) : (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
• ArithmeticFunction.IsMultiplicative.eulerProduct 📋 Mathlib.NumberTheory.EulerProduct.Basic
  {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable fun x => ‖f x‖) : Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ℕ), f n))
• riemannZeta_eulerProduct 📋 Mathlib.NumberTheory.EulerProduct.DirichletLSeries
  {s : ℂ} (hs : 1 < s.re) : Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) Filter.atTop (nhds (riemannZeta s))
• dirichletLSeries_eulerProduct 📋 Mathlib.NumberTheory.EulerProduct.DirichletLSeries
  {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (LSeries (fun n => χ ↑n) s))
• DirichletCharacter.LSeries_eulerProduct 📋 Mathlib.NumberTheory.EulerProduct.DirichletLSeries
  {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (LSeries (fun n => χ ↑n) s))
• DirichletCharacter.LSeries_changeLevel 📋 Mathlib.NumberTheory.EulerProduct.DirichletLSeries
  {M N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) : LSeries (fun n => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s = LSeries (fun n => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
• NumberField.mixedEmbedding.volume_eq_two_pi_pow_mul_integral 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
  {K : Type u_1} [Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)} [NumberField K] (hA : NumberField.mixedEmbedding.normAtComplexPlaces ⁻¹' (NumberField.mixedEmbedding.normAtComplexPlaces '' A) = A) (hm : MeasurableSet A) : MeasureTheory.volume A = ENNReal.ofReal (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in NumberField.mixedEmbedding.normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)
• NumberField.mixedEmbedding.volume_eq_two_pow_mul_two_pi_pow_mul_integral 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
  {K : Type u_1} [Field K] {A : Set (NumberField.mixedEmbedding.mixedSpace K)} [NumberField K] (hA : NumberField.mixedEmbedding.normAtAllPlaces ⁻¹' (NumberField.mixedEmbedding.normAtAllPlaces '' A) = A) (hm : MeasurableSet A) : MeasureTheory.volume A = 2 ^ NumberField.InfinitePlace.nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in NumberField.mixedEmbedding.normAtAllPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)
• NumberField.mixedEmbedding.fundamentalCone.prod_expMapBasis_pow 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
  {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.realSpace K) : ∏ w, ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x w ^ w.mult = Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) ^ Module.finrank ℚ K
• NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
  (K : Type u_1) [Field K] [NumberField K] (x : NumberField.mixedEmbedding.realSpace K) : |(NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis K x).det| = Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K)) * (∏ w, ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K) * NumberField.Units.regulator K
• NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply' 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
  {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.realSpace K) : ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x = Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) • fun w => ∏ i, w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.fundSystem K (NumberField.mixedEmbedding.fundamentalCone.equivFinRank.symm i))) ^ x ↑i
• NumberField.mixedEmbedding.fundamentalCone.setLIntegral_expMapBasis_image 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
  {K : Type u_1} [Field K] [NumberField K] {s : Set (NumberField.mixedEmbedding.realSpace K)} (hs : MeasurableSet s) {f : (NumberField.InfinitePlace K → ℝ) → ENNReal} (hf : Measurable f) : ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis '' s, f x = 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * ENNReal.ofReal (NumberField.Units.regulator K) * ↑(Module.finrank ℚ K) * ∫⁻ (x : NumberField.mixedEmbedding.realSpace K) in s, ENNReal.ofReal (Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀ * ↑(Module.finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis (fun w => x w) ↑i))⁻¹ * f (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x)
• NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single 📋 Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
  {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.realSpace K) : ∏ w, NumberField.mixedEmbedding.fundamentalCone.deriv_expMap_single w ((NumberField.mixedEmbedding.fundamentalCone.completeBasis K).equivFun.symm x w) = Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) ^ Module.finrank ℚ K * (∏ w, ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K
• NumberField.prod_abs_eq_one 📋 Mathlib.NumberTheory.NumberField.ProductFormula
  {K : Type u_1} [Field K] [NumberField K] {x : K} (h_x_nezero : x ≠ 0) : (∏ w, w x ^ w.mult) * ∏ᶠ (w : NumberField.FinitePlace K), w x = 1

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