instance AddCircle.noAtoms_volume (T : ℝ) [hT : Fact (0 < T)] : MeasureTheory.NullSingletonClass MeasureTheory.volume

theorem AddCircle.liftIoc_ae_eq_liftIco {B : Type u_1} {T a : ℝ} [hT : Fact (0 < T)] (f : ℝ → B) : liftIoc T a f =ᵐ[MeasureTheory.volume] liftIco T a f

theorem AddCircle.measurable_equivIoc (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : Measurable ⇑(equivIoc T a)

theorem AddCircle.measurable_equivIco (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : Measurable ⇑(equivIco T a)

noncomputable def AddCircle.measurableEquivIoc' (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : AddCircle T ≃ᵐ ↑(Set.Ioc a (a + T))

Equations

• AddCircle.measurableEquivIoc' T a = { toEquiv := AddCircle.equivIoc T a, measurable_toFun := ⋯, measurable_invFun := ⋯ }

noncomputable def AddCircle.measurableEquivIco' (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) : AddCircle T ≃ᵐ ↑(Set.Ico a (a + T))

Equations

• AddCircle.measurableEquivIco' T a = { toEquiv := AddCircle.equivIco T a, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem AddCircle.map_subtypeVal_map_equivIoc_volume (T a : ℝ) [hT : Fact (0 < T)] : MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.map (⇑(equivIoc T a)) MeasureTheory.volume) = MeasureTheory.volume.restrict (Set.Ioc a (a + T))

theorem MeasureTheory.AEStronglyMeasurable.liftIoc {E : Type u_1} (T a : ℝ) [hT : Fact (0 < T)] {f : ℝ → E} [TopologicalSpace E] (hf : AEStronglyMeasurable f volume) : AEStronglyMeasurable (AddCircle.liftIoc T a f) volume

theorem MeasureTheory.AEStronglyMeasurable.liftIco {E : Type u_1} (T a : ℝ) [hT : Fact (0 < T)] {f : ℝ → E} [TopologicalSpace E] (hf : AEStronglyMeasurable f volume) : AEStronglyMeasurable (AddCircle.liftIco T a f) volume

theorem MeasureTheory.AEMeasurable.liftIoc {E : Type u_1} (T a : ℝ) [hT : Fact (0 < T)] {f : ℝ → E} [MeasurableSpace E] (hf : AEMeasurable f volume) : AEMeasurable (AddCircle.liftIoc T a f) volume

theorem MeasureTheory.AEMeasurable.liftIco {E : Type u_1} (T a : ℝ) [hT : Fact (0 < T)] {f : ℝ → E} [MeasurableSpace E] (hf : AEMeasurable f volume) : AEMeasurable (AddCircle.liftIco T a f) volume

theorem MeasureTheory.map_coe_addCircle_volume_eq (T : ℝ) [hT : Fact (0 < T)] : Measure.map (fun (x : ℝ) => ↑x) volume = ⊤ • volume

theorem MeasureTheory.quasiMeasurePreserving_coe_addCircle (T : ℝ) [hT : Fact (0 < T)] : QuasiMeasurePreserving (fun (x : ℝ) => ↑x) volume volume

theorem AddCircle.liftIco_convolution_liftIco {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [NormedSpace ℝ F] (L : E →L[𝕜] E' →L[𝕜] F) {f : ℝ → E} {g : ℝ → E'} {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) (hf : Function.Periodic f T) (hg : Function.Periodic g T) : MeasureTheory.convolution (liftIco T a f) (liftIco T a g) L MeasureTheory.volume = liftIco T a fun (x : ℝ) => ∫ (y : ℝ) in a..a + T, (L (f y)) (g (x - y))

theorem AddCircle.liftIoc_convolution_liftIoc {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F] [NormedSpace ℝ F] (L : E →L[𝕜] E' →L[𝕜] F) {f : ℝ → E} {g : ℝ → E'} {T : ℝ} [hT : Fact (0 < T)] (a : ℝ) (hf : Function.Periodic f T) (hg : Function.Periodic g T) : MeasureTheory.convolution (liftIoc T a f) (liftIoc T a g) L MeasureTheory.volume = liftIoc T a fun (x : ℝ) => ∫ (y : ℝ) in a..a + T, (L (f y)) (g (x - y))

theorem AddCircle.eLpNorm_liftIoc {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (p : ENNReal) : MeasureTheory.eLpNorm (liftIoc T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm ((Set.Ioc a (a + T)).indicator f) p MeasureTheory.volume

The norm of the lift of a function f is equal to the norm of f on that period.

theorem AddCircle.eLpNorm_liftIoc' {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (p : ENNReal) : MeasureTheory.eLpNorm (liftIoc T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc a (a + T)))

The norm of the lift of a function f is equal to the norm of f on that period.

theorem AddCircle.eLpNorm_liftIco {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (p : ENNReal) : MeasureTheory.eLpNorm (liftIco T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm ((Set.Ico a (a + T)).indicator f) p MeasureTheory.volume

The norm of the lift of a function f is equal to the norm of f on that period.

theorem AddCircle.eLpNorm_liftIco' {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (p : ENNReal) : MeasureTheory.eLpNorm (liftIco T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ico a (a + T)))

The norm of the lift of a function f is equal to the norm of f on that period.

theorem AddCircle.eLpNorm_liftIoc_of_periodic {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a a' : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hfT : Function.Periodic f T) (p : ENNReal) : MeasureTheory.eLpNorm (liftIoc T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm ((Set.Ioc a' (a' + T)).indicator f) p MeasureTheory.volume

The norm of the lift of a periodic function f is equal to the norm of f on any period.

theorem AddCircle.eLpNorm_liftIoc_of_periodic' {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a a' : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hfT : Function.Periodic f T) (p : ENNReal) : MeasureTheory.eLpNorm (liftIoc T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ioc a' (a' + T)))

The norm of the lift of a periodic function f is equal to the norm of f on any period.

theorem AddCircle.eLpNorm_liftIco_of_periodic {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a a' : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hfT : Function.Periodic f T) (p : ENNReal) : MeasureTheory.eLpNorm (liftIco T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm ((Set.Ico a' (a' + T)).indicator f) p MeasureTheory.volume

The norm of the lift of a periodic function f is equal to the norm of f on any period.

theorem AddCircle.eLpNorm_liftIco_of_periodic' {B : Type u_2} [NormedAddCommGroup B] (T : ℝ) [hT : Fact (0 < T)] (a a' : ℝ) {f : ℝ → B} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hfT : Function.Periodic f T) (p : ENNReal) : MeasureTheory.eLpNorm (liftIco T a f) p MeasureTheory.volume = MeasureTheory.eLpNorm f p (MeasureTheory.volume.restrict (Set.Ico a' (a' + T)))

The norm of the lift of a periodic function f is equal to the norm of f on any period.