noncomputable instance NNReal.MeasureSpace : MeasureTheory.MeasureSpace NNReal

Equations

• NNReal.MeasureSpace = { toMeasurableSpace := MeasureTheory.Measure.Subtype.measureSpace.toMeasurableSpace, volume := MeasureTheory.volume }

theorem NNReal.volume_val {s : Set NNReal} : MeasureTheory.volume s = MeasureTheory.volume (Subtype.val '' s)

noncomputable instance instMeasureSpaceENNReal_carleson : MeasureTheory.MeasureSpace ENNReal

Equations

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

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)

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

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_Ioo_eq_Ioo {a b : NNReal} : toReal '' Set.Ioo a b = Set.Ioo ↑a ↑b

theorem NNReal.volume_Iio {b : NNReal} : MeasureTheory.volume (Set.Iio b) = ↑b

theorem NNReal.volume_Ioo {a b : NNReal} : MeasureTheory.volume (Set.Ioo a b) = ↑b - ↑a

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.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_Ioo {a b : ENNReal} (ha : a ≠ ⊤) : MeasureTheory.volume (Set.Ioo a b) = b - a

instance instIsOpenPosMeasureENNRealVolume_carleson : MeasureTheory.volume.IsOpenPosMeasure

instance instIsOpenPosMeasureNNRealVolume_carleson : MeasureTheory.volume.IsOpenPosMeasure

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 lintegral_nnreal_eq_lintegral_Ici_ofReal {f : NNReal → ENNReal} : ∫⁻ (x : NNReal), f x = ∫⁻ (x : ℝ) in Set.Ici 0, 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 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