Structures · Analysis
MeasureTheory.Measure.HasTemperateGrowth
A measure μ has temperate growth if there is an n : ℕ such that (1 + ‖x‖) ^ (- n) is
μ-integrable.
- Shape
- One type argument · adds exists_integrable
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by50
- SchwartzMap.toLp
- MeasureTheory.Lp.toTemperedDistribution
- SchwartzMap.toTemperedDistributionCLM
- SchwartzMap.integrable
- MeasureTheory.Lp.toTemperedDistributionCLM
- SchwartzMap.toTemperedDistributionCLM_apply_apply
- SchwartzMap.toLpCLM
- SchwartzMap.coeFn_toLp
- MeasureTheory.Lp.toTemperedDistributionCLM_apply
- MeasureTheory.Measure.toTemperedDistribution
- MeasureTheory.Lp.toTemperedDistribution_apply
- SchwartzMap.denseRange_toLpCLM
- SchwartzMap.memLp
- SchwartzMap.norm_toLp
- SchwartzMap.integralCLM
- MeasureTheory.Lp.toTemperedDistribution_toLp_eq
- MeasureTheory.Measure.toTemperedDistribution_apply
- SchwartzMap.integrable_pow_mul
- MeasureTheory.Lp.toTemperedDistribution_smul_eq
- SchwartzMap.eLpNorm_le_seminorm
- MeasureTheory.Measure.integrable_pow_neg_integrablePower
- MeasureTheory.Measure.HasTemperateGrowth.exists_integrable
- SchwartzMap.integralCLM_apply
- MeasureTheory.Lp.toTemperedDistribution.congr_simp
- SchwartzMap.norm_toLp_top_le
- SchwartzMap.norm_toLp'
- integral_pow_mul_le_of_le_of_pow_mul_le
- Function.HasTemperateGrowth.toTemperedDistribution
- SchwartzMap.norm_toLp_one
- SchwartzMap.eLpNorm_lt_top
- SchwartzMap.integrable_pow_mul_iteratedFDeriv
- integrable_of_le_of_pow_mul_le
- SchwartzMap.toLp.congr_simp
- SchwartzMap.inner_toL2_toL2_eq
- MeasureTheory.Lp.toTemperedDistributionCLM.congr_simp
- SchwartzMap.norm_toLp_le_seminorm
- MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot
- Function.HasTemperateGrowth.toTemperedDistribution_apply
- SchwartzMap.toTemperedDistributionCLM.congr_simp
- SchwartzMap.integralCLM.congr_simp
- SchwartzMap.toLpCLM.congr_simp
- SchwartzMap.integral_pow_mul_iteratedFDeriv_le
- SchwartzMap.coe_apply
- SchwartzMap.toLpCLM_apply
- MeasureTheory.Lp.instCoeToTemperedDistribution
- SchwartzMap.injective_toLp
- MeasureTheory.Measure.toTemperedDistribution.congr_simp
- SchwartzMap.instCoeToLp
- SchwartzMap.instCoeToTemperedDistribution
- SchwartzMap.continuous_toLp
Ancestors0
No ancestors.