LeanPool.SardMoreira.WithRPowDist #
@[implicit_reducible]
instance
WithRPowDist.instMeasurableSpace
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
MeasurableSpace (WithRPowDist X α hα₀ hα₁)
Equations
theorem
WithRPowDist.measurable_val
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
theorem
WithRPowDist.measurable_mk
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
def
WithRPowDist.measurableEquiv
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
The natural measurable equivalence between WithRPowDist X α hα₀ hα₁ and X.
Equations
- WithRPowDist.measurableEquiv = { toEquiv := WithRPowDist.equiv X α hα₀ hα₁, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
@[simp]
theorem
WithRPowDist.measurableEquiv_apply
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
@[simp]
theorem
WithRPowDist.measurableEquiv_toEquiv
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
@[simp]
theorem
WithRPowDist.measurableEquiv_symm_apply
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
theorem
WithRPowDist.measurableEmbedding_mk
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
:
instance
WithRPowDist.instBorelSpace
{X : Type u_1}
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[MeasurableSpace X]
[TopologicalSpace X]
[BorelSpace X]
:
BorelSpace (WithRPowDist X α hα₀ hα₁)
noncomputable def
MeasureTheory.Measure.withRPowDist
{X : Type u_1}
[MeasurableSpace X]
(α : ℝ)
(hα₀ : 0 < α)
(hα₁ : α ≤ 1)
(μ : Measure X)
:
Measure (WithRPowDist X α hα₀ hα₁)
The pushforward of a measure μ on X under the canonical map
X → WithRPowDist X α hα₀ hα₁.
Equations
Instances For
theorem
MeasureTheory.Measure.withRPowDist_apply
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
(μ : Measure X)
(s : Set (WithRPowDist X α hα₀ hα₁))
:
instance
MeasureTheory.Measure.instIsFiniteMeasureWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[IsFiniteMeasure μ]
:
IsFiniteMeasure (withRPowDist α hα₀ hα₁ μ)
instance
MeasureTheory.Measure.instSigmaFiniteWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[SigmaFinite μ]
:
SigmaFinite (withRPowDist α hα₀ hα₁ μ)
instance
MeasureTheory.Measure.instSFiniteWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[SFinite μ]
:
SFinite (withRPowDist α hα₀ hα₁ μ)
instance
MeasureTheory.Measure.instIsLocallyFiniteMeasureWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[IsLocallyFiniteMeasure μ]
:
IsLocallyFiniteMeasure (withRPowDist α hα₀ hα₁ μ)
instance
MeasureTheory.Measure.instIsFiniteMeasureOnCompactsWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[IsFiniteMeasureOnCompacts μ]
:
IsFiniteMeasureOnCompacts (withRPowDist α hα₀ hα₁ μ)
instance
MeasureTheory.Measure.instOuterRegularWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[μ.OuterRegular]
:
(withRPowDist α hα₀ hα₁ μ).OuterRegular
instance
MeasureTheory.Measure.instInnerRegularWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[μ.InnerRegular]
:
(withRPowDist α hα₀ hα₁ μ).InnerRegular
instance
MeasureTheory.Measure.instWeaklyRegularWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[μ.WeaklyRegular]
:
(withRPowDist α hα₀ hα₁ μ).WeaklyRegular
instance
MeasureTheory.Measure.instInnerRegularCompactLTTopWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[μ.InnerRegularCompactLTTop]
:
(withRPowDist α hα₀ hα₁ μ).InnerRegularCompactLTTop
instance
MeasureTheory.Measure.instRegularWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[TopologicalSpace X]
[μ.Regular]
:
(withRPowDist α hα₀ hα₁ μ).Regular
@[simp]
theorem
MeasureTheory.Measure.withRPowDist_hausdorffMeasure
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
[EMetricSpace X]
[BorelSpace X]
(d : ℝ)
:
instance
MeasureTheory.Measure.instIsUnifLocDoublingMeasureWithRPowDistWithRPowDist
{X : Type u_1}
[MeasurableSpace X]
{α : ℝ}
{hα₀ : 0 < α}
{hα₁ : α ≤ 1}
{μ : Measure X}
[PseudoMetricSpace X]
[IsUnifLocDoublingMeasure μ]
:
IsUnifLocDoublingMeasure (withRPowDist α hα₀ hα₁ μ)