Documentation

Carleson.ToMathlib.MeasureTheory.Measure.NNReal

@[implicit_reducible]

noncomputable instance NNReal.MeasureSpace :

MeasureTheory.MeasureSpace NNReal

Equations

NNReal.MeasureSpace = { toMeasurableSpace := NNReal.measurableSpace, volume := MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume }

theorem NNReal.volume_val {s : Set NNReal} :

MeasureTheory.volume s = MeasureTheory.volume (Subtype.val '' s)

@[implicit_reducible]

noncomputable instance instMeasureSpaceENNReal_carleson :

MeasureTheory.MeasureSpace ENNReal

Equations

instMeasureSpaceENNReal_carleson = { toMeasurableSpace := ENNReal.measurableSpace, volume := MeasureTheory.Measure.map ENNReal.ofNNReal MeasureTheory.volume }

theorem ENNReal.ofNNReal_preimage {s : Set ENNReal} :

ofNNReal ⁻¹' s = ENNReal.toNNReal '' (s \ {⊤})

theorem ENNReal.map_toReal_eq_map_toReal_comap_ofReal {s : Set ENNReal} (h : ⊤ ∉ s) :

ENNReal.toReal '' s = NNReal.toReal '' ofNNReal ⁻¹' s

theorem ENNReal.map_toReal_eq_map_toReal_comap_ofReal' {s : Set ENNReal} (h : ⊤ ∈ s) :

ENNReal.toReal '' s = NNReal.toReal '' ofNNReal ⁻¹' s ∪ {0}

theorem ENNReal.map_toReal_ae_eq_map_toReal_comap_ofReal {s : Set ENNReal} :

ENNReal.toReal '' s =ᵐ[MeasureTheory.volume ] NNReal.toReal '' ofNNReal ⁻¹' s

theorem ENNReal.volume_val {s : Set ENNReal} (hs : MeasurableSet s) :

MeasureTheory.volume s = MeasureTheory.volume (ENNReal.toReal '' s)

instance instNoAtomsENNRealVolume_carleson :

MeasureTheory.NoAtoms MeasureTheory.volume

theorem Measure.Subtype.noAtoms {δ : Type u_1} [MeasureTheory.MeasureSpace δ] [MeasureTheory.NoAtoms MeasureTheory.volume] {p : δ → Prop} (hp : MeasurableSet p) :

MeasureTheory.NoAtoms MeasureTheory.volume

instance instNoAtomsNNRealVolume_carleson :

MeasureTheory.NoAtoms MeasureTheory.volume

theorem Measure.Subtype.sigmaFinite {δ : Type u_1} [MeasureTheory.MeasureSpace δ] [sf : MeasureTheory.SigmaFinite MeasureTheory.volume] {p : δ → Prop} (hp : MeasurableSet p) :

MeasureTheory.SigmaFinite MeasureTheory.volume

instance instSigmaFiniteNNRealVolume_carleson :

MeasureTheory.SigmaFinite MeasureTheory.volume

theorem measurableEmbedding_ofNNReal :

MeasurableEmbedding ENNReal.ofNNReal

instance instSigmaFiniteENNRealVolume_carleson :

MeasureTheory.SigmaFinite MeasureTheory.volume

theorem NNReal.volume_eq_volume_ennreal {s : Set NNReal} (hs : MeasurableSet (ENNReal.ofNNReal '' s)) :

MeasureTheory.volume s = MeasureTheory.volume (ENNReal.ofNNReal '' s)

theorem NNReal.smul_map_volume_mul_left {a : NNReal} (h : a ≠ 0) :

a • MeasureTheory.Measure.map (fun (x : NNReal) => a * x) MeasureTheory.volume = MeasureTheory.volume

theorem NNReal.map_volume_mul_left {a : NNReal} (h : a ≠ 0) :

MeasureTheory.Measure.map (fun (x : NNReal) => a * x) MeasureTheory.volume = a⁻¹ • MeasureTheory.volume

theorem ENNReal.volume_eq_volume_preimage {s : Set ENNReal} (hs : MeasurableSet s) :

MeasureTheory.volume s = MeasureTheory.volume (ENNReal.ofReal ⁻¹' s ∩ Set.Ici 0)

theorem Ioo_zero_top_ae_eq_univ :

Set.Ioo 0 ⊤ =ᵐ[MeasureTheory.volume ] Set.univ

theorem ae_in_Ioo_zero_top :

∀ᵐ (x : ENNReal), x ∈ Set.Ioo 0 ⊤

theorem map_restrict_Ioi_eq_restrict_Ioi :

MeasureTheory.Measure.map ENNReal.ofReal (MeasureTheory.volume.restrict (Set.Ioi 0)) = MeasureTheory.volume.restrict (Set.Ioi 0)

theorem map_restrict_Ioi_eq_volume :

MeasureTheory.Measure.map ENNReal.ofReal (MeasureTheory.volume.restrict (Set.Ioi 0)) = MeasureTheory.volume

theorem NNReal.toReal_Iio_eq_Ico {b : NNReal} :

toReal '' Set.Iio b = Set.Ico 0 ↑b

theorem NNReal.toReal_Ioi_eq_Ioi {b : NNReal} :

toReal '' Set.Ioi b = Set.Ioi ↑b

theorem NNReal.toReal_Ioo_eq_Ioo {a b : NNReal} :

toReal '' Set.Ioo a b = Set.Ioo ↑a ↑b

theorem NNReal.Ici_eq {a : NNReal} :

Set.Ici ↑a = Real.toNNReal ⁻¹' Set.Ici a ∩ Set.Ici 0

theorem NNReal.volume_Iio {b : NNReal} :

MeasureTheory.volume (Set.Iio b) = ↑b

theorem NNReal.volume_Ioi {b : NNReal} :

MeasureTheory.volume (Set.Ioi b) = ⊤

theorem NNReal.volume_Ioo {a b : NNReal} :

MeasureTheory.volume (Set.Ioo a b) = ↑b - ↑a

theorem ENNReal.toReal_Iio_eq_Ico {a : ENNReal} (ha : a ≠ ⊤) :

ENNReal.toReal '' Set.Iio a = Set.Ico 0 a.toReal

theorem ENNReal.toReal_Iio_top_eq_Ici :

ENNReal.toReal '' Set.Iio ⊤ = Set.Ici 0

theorem ENNReal.toReal_Icc_eq_Icc {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal '' Set.Icc a b = Set.Icc a.toReal b.toReal

theorem ENNReal.toReal_Ioo_eq_Ioo {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

ENNReal.toReal '' Set.Ioo a b = Set.Ioo a.toReal b.toReal

theorem ENNReal.toReal_Ioo_top_eq_Ioi {a : ENNReal} (ha : a ≠ ⊤) :

ENNReal.toReal '' Set.Ioo a ⊤ = Set.Ioi a.toReal

theorem ENNReal.toReal_Ioi_eq_Ioi {a : ENNReal} (ha : a ≠ ⊤) :

ENNReal.toReal '' Set.Ioi a = Set.Ioi a.toReal ∪ {0}

theorem ENNReal.ofReal_Ioo_eq {a b : ENNReal} :

ENNReal.ofReal ⁻¹' Set.Ioo a b = if a = ⊤ then ∅ else if a ≤ b ∧ b = ⊤ then Set.Ioi a.toReal else Set.Ioo a.toReal b.toReal

theorem ENNReal.ofReal_Iio_eq {b : ENNReal} :

ENNReal.ofReal ⁻¹' Set.Iio b = if b = 0 then ∅ else if b = ⊤ then Set.univ else Set.Iio b.toReal

theorem ENNReal.toNNReal_Iio {b : ENNReal} :

ENNReal.toNNReal '' Set.Iio b = if b = ⊤ then Set.univ else Set.Iio b.toNNReal

theorem ENNReal.volume_Ioi {a : ENNReal} (ha : a ≠ ⊤) :

MeasureTheory.volume (Set.Ioi a) = ⊤

theorem ENNReal.Ioi_eq_Ioc_top {a : ENNReal} :

Set.Ioi a = Set.Ioc a ⊤

theorem ENNReal.volume_Iio {a : ENNReal} :

MeasureTheory.volume (Set.Iio a) = a

@[simp]

theorem ENNReal.range_toReal :

Set.range ENNReal.toReal = Set.Ici 0

@[simp]

theorem ENNReal.volume_univ :

MeasureTheory.volume Set.univ = ⊤

@[simp]

theorem ENNReal.volume_Iic {a : ENNReal} :

MeasureTheory.volume (Set.Iic a) = a

theorem ENNReal.volume_Ioo {a b : ENNReal} :

MeasureTheory.volume (Set.Ioo a b) = b - a

instance instIsOpenPosMeasureENNRealVolume_carleson :

MeasureTheory.volume.IsOpenPosMeasure

instance instIsOpenPosMeasureNNRealVolume_carleson :

MeasureTheory.volume.IsOpenPosMeasure

theorem ENNReal.volume_map_add_left_le_self {g : ENNReal} (hg : g ≠ ⊤) {s : Set ENNReal} (hs : MeasurableSet s) :

(MeasureTheory.Measure.map (fun (x : ENNReal) => g + x) MeasureTheory.volume) s ≤ MeasureTheory.volume s

theorem ENNReal.volume_map_add_right_le_self {g : ENNReal} (hg : g ≠ ⊤) {s : Set ENNReal} (hs : MeasurableSet s) :

(MeasureTheory.Measure.map (fun (x : ENNReal) => x + g) MeasureTheory.volume) s ≤ MeasureTheory.volume s

theorem ENNReal.volume_Ico {a b : ENNReal} :

MeasureTheory.volume (Set.Ico a b) = b - a

theorem lintegral_nnreal_eq_lintegral_Ici_ofReal {f : NNReal → ENNReal} :

∫⁻ (x : NNReal), f x = ∫⁻ (x : ℝ) in Set.Ici 0, f x.toNNReal

theorem lintegral_nnreal_Ici_eq_lintegral_Ici_ofReal {f : NNReal → ENNReal} {a : NNReal} :

∫⁻ (x : NNReal) in Set.Ici a, f x = ∫⁻ (x : ℝ) in Set.Ici ↑a, f x.toNNReal

theorem lintegral_nnreal_eq_lintegral_Ioi_ofReal {f : ENNReal → ENNReal} :

∫⁻ (x : NNReal), f ↑x = ∫⁻ (x : ℝ) in Set.Ioi 0, f (ENNReal.ofReal x)

theorem lintegral_ennreal_eq_lintegral_of_nnreal {f : ENNReal → ENNReal} :

∫⁻ (x : ENNReal), f x = ∫⁻ (x : NNReal), f ↑x

theorem setLIntegral_ennreal_eq_setLintegral_of_nnreal {f : ENNReal → ENNReal} {s : Set ENNReal} (hs : MeasurableSet s) :

∫⁻ (x : ENNReal) in s, f x = ∫⁻ (x : NNReal) in ENNReal.ofNNReal ⁻¹' s, f ↑x

theorem lintegral_ennreal_eq_lintegral_Ioi_ofReal {f : ENNReal → ENNReal} :

∫⁻ (x : ENNReal), f x = ∫⁻ (x : ℝ) in Set.Ioi 0, f (ENNReal.ofReal x)

theorem lintegral_nnreal_eq_lintegral_toNNReal_Ioi (f : NNReal → ENNReal) :

∫⁻ (x : NNReal), f x = ∫⁻ (x : ℝ) in Set.Ioi 0, f x.toNNReal

theorem lintegral_nnreal_toReal_eq_lintegral_Ioi (f : ℝ → ENNReal) :

∫⁻ (x : NNReal), f ↑x = ∫⁻ (x : ℝ) in Set.Ioi 0, f x

theorem lintegral_nnreal_toReal_eq_lintegral_Ici (f : ℝ → ENNReal) :

∫⁻ (x : NNReal), f ↑x = ∫⁻ (x : ℝ) in Set.Ici 0, f x

theorem setLIntegral_nnreal_Ici {f : NNReal → ENNReal} {a : NNReal} :

∫⁻ (t : NNReal) in Set.Ici a, f t = ∫⁻ (t : NNReal), f (t + a)

theorem lintegral_nnreal_scale_constant' {f : NNReal → ENNReal} {a : NNReal} (h : a ≠ 0) :

↑a * ∫⁻ (x : NNReal), f (a * x) = ∫⁻ (x : NNReal), f x