Theorems · Theorem · measure theory
AEMeasurable.pow_const
∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
[inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β},
AEMeasurable f μ → ∀ (c : γ), AEMeasurable (fun x => f x ^ c) μ- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- AEMeasurablestatement and proof · cited by 840
- aemeasurable_constproof · cited by 22
- MeasurablePowstatement and proof · cited by 9
- AEMeasurable.powproof · cited by 4
Cited by27
Results whose statement or proof uses this declaration.
- ProbabilityTheory.variance_eq_integralproof · cited by 10
- MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_normproof · cited by 4
- MeasureTheory.eLpNorm_map_measureproof · cited by 3
- MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNormproof · cited by 3
- MeasureTheory.lpNorm_eq_integral_norm_rpow_toRealproof · cited by 3
- MeasureTheory.MemLp.norm_rpow_divproof · cited by 2
- MeasureTheory.MemLp.enorm_rpow_divproof · cited by 2
- MeasureTheory.pow_mul_meas_ge_le_eLpNormproof · cited by 2
- ENNReal.lintegral_Lp_mul_le_Lq_mul_Lrproof · cited by 2
- MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zeroproof · cited by 1
- MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mulproof · cited by 1
- MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm'proof · cited by 1