Locally Bounded Functions #
This file develops the theory of locally bounded functions, and relates it to local integrability.
In particular:
- A measurable locally bounded function is locally integrable.
TODO:
- Relate to Continuous / ContinuousOn (and ContinuousAt for BoundedAtFilter)
theorem
MeasureTheory.IntegrableAtFilter.mul_boundedAtFilter
{α : Type u_1}
{ε' : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
[NormedRing ε']
{l : Filter α}
(hl : l.IsMeasurablyGenerated)
{f g : α → ε'}
(hg_meas : AEStronglyMeasurable g μ)
(hf : IntegrableAtFilter f l μ)
(hg : l.BoundedAtFilter g)
:
IntegrableAtFilter (f * g) l μ
theorem
MeasureTheory.IntegrableAtFilter.boundedAtFilter_mul
{α : Type u_1}
{ε' : Type u_2}
{mα : MeasurableSpace α}
{μ : Measure α}
[NormedRing ε']
{l : Filter α}
(hl : l.IsMeasurablyGenerated)
{f g : α → ε'}
(hg_meas : AEStronglyMeasurable g μ)
(hf : IntegrableAtFilter f l μ)
(hg : l.BoundedAtFilter g)
:
IntegrableAtFilter (g * f) l μ
theorem
Filter.BoundedAtFilter.integrableAtFilter
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
{f : α → β}
{l : Filter α}
(hl : l.IsMeasurablyGenerated)
(hμ : μ.FiniteAtFilter l)
(hf : l.BoundedAtFilter f)
(hf_meas : StronglyMeasurableAtFilter f l μ)
:
theorem
Filter.BoundedAtFilter.integrableAtFilter_nhds
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : α → β}
(a : α)
(hf : (nhds a).BoundedAtFilter f)
(hf_meas : StronglyMeasurableAtFilter f (nhds a) μ)
:
MeasureTheory.IntegrableAtFilter f (nhds a) μ
theorem
Filter.BoundedAtFilter.integrableAtFilter_nhdsWithin
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : α → β}
{s : Set α}
(hs : MeasurableSet s)
{a : α}
(hf : (nhdsWithin a s).BoundedAtFilter f)
(hf_meas : StronglyMeasurableAtFilter f (nhdsWithin a s) μ)
:
MeasureTheory.IntegrableAtFilter f (nhdsWithin a s) μ
structure
IsLocallyBounded
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Norm β]
(f : α → β)
:
- locally_bdd' (x : α) : (nhds x).BoundedAtFilter f
Instances For
theorem
IsLocallyBounded.boundedAtFilter
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Norm β]
{f : α → β}
(hf : IsLocallyBounded f)
(x : α)
:
(nhds x).BoundedAtFilter f
theorem
IsLocallyBounded.locallyIntegrable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[NormedAddCommGroup β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsLocallyFiniteMeasure μ]
(f : α → β)
(hf_bdd : IsLocallyBounded f)
(hf_meas : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.LocallyIntegrable.mul_isLocallyBounded
{X : Type u_1}
{R : Type u_2}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
[NormedRing R]
[SecondCountableTopologyEither X R]
{f g : X → R}
(hf : LocallyIntegrable f μ)
(hg : IsLocallyBounded g)
(hg_meas : AEStronglyMeasurable g μ)
:
LocallyIntegrable (fun (x : X) => f x * g x) μ
theorem
MeasureTheory.LocallyIntegrable.isLocallyBounded_mul
{X : Type u_1}
{R : Type u_2}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
[NormedRing R]
[SecondCountableTopologyEither X R]
{f g : X → R}
(hf : LocallyIntegrable f μ)
(hg : IsLocallyBounded g)
(hg_meas : AEStronglyMeasurable g μ)
:
LocallyIntegrable (fun (x : X) => g x * f x) μ
theorem
const_isLocallyBounded
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
(c : β)
:
IsLocallyBounded fun (x : α) => c
theorem
IsLocallyBounded.add
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f g : α → β}
(hf : IsLocallyBounded f)
(hg : IsLocallyBounded g)
:
IsLocallyBounded fun (x : α) => f x + g x
theorem
IsLocallyBounded.sub
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f g : α → β}
(hf : IsLocallyBounded f)
(hg : IsLocallyBounded g)
:
IsLocallyBounded fun (x : α) => f x - g x
theorem
IsLocallyBounded.neg
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f : α → β}
(hf : IsLocallyBounded f)
:
IsLocallyBounded fun (x : α) => -f x
theorem
IsLocallyBounded.smul
{α : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
[TopologicalSpace α]
[SeminormedRing 𝕜]
[SeminormedAddCommGroup β]
[Module 𝕜 β]
[IsBoundedSMul 𝕜 β]
{f : α → β}
(c : 𝕜)
(hf : IsLocallyBounded f)
:
IsLocallyBounded fun (x : α) => c • f x
theorem
IsLocallyBounded.mul
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedRing β]
{f g : α → β}
(hf : IsLocallyBounded f)
(hg : IsLocallyBounded g)
:
IsLocallyBounded fun (x : α) => f x * g x
theorem
IsLocallyBounded.norm
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f : α → β}
(hf : IsLocallyBounded f)
:
IsLocallyBounded fun (x : α) => ‖f x‖
structure
IsLocallyBoundedOn
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Norm β]
(f : α → β)
(s : Set α)
:
- locally_bddOn' (x : α) : x ∈ s → (nhdsWithin x s).BoundedAtFilter f
Instances For
theorem
IsLocallyBoundedOn.boundedAtFilter
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Norm β]
{f : α → β}
{s : Set α}
(hf : IsLocallyBoundedOn f s)
{x : α}
(hx : x ∈ s)
:
(nhdsWithin x s).BoundedAtFilter f
theorem
IsLocallyBoundedOn.locallyIntegrableOn
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[NormedAddCommGroup β]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{f : α → β}
{s : Set α}
(hs : MeasurableSet s)
(hf_bdd : IsLocallyBoundedOn f s)
(hf_meas : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.LocallyIntegrableOn.mul_isLocallyBoundedOn
{X : Type u_1}
{R : Type u_2}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
[NormedRing R]
[SecondCountableTopologyEither X R]
{f g : X → R}
{s : Set X}
(hs : MeasurableSet s)
(hf : LocallyIntegrableOn f s μ)
(hg : IsLocallyBoundedOn g s)
(hg_meas : AEStronglyMeasurable g μ)
:
LocallyIntegrableOn (fun (x : X) => f x * g x) s μ
theorem
MeasureTheory.LocallyIntegrableOn.isLocallyBoundedOn_mul
{X : Type u_1}
{R : Type u_2}
[MeasurableSpace X]
[TopologicalSpace X]
{μ : Measure X}
[OpensMeasurableSpace X]
[LocallyCompactSpace X]
[T2Space X]
[NormedRing R]
[SecondCountableTopologyEither X R]
{f g : X → R}
{s : Set X}
(hs : MeasurableSet s)
(hf : LocallyIntegrableOn f s μ)
(hg : IsLocallyBoundedOn g s)
(hg_meas : AEStronglyMeasurable g μ)
:
LocallyIntegrableOn (fun (x : X) => g x * f x) s μ
theorem
const_isLocallyBoundedOn
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
(c : β)
(s : Set α)
:
IsLocallyBoundedOn (fun (x : α) => c) s
theorem
IsLocallyBoundedOn.add
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f g : α → β}
{s : Set α}
(hf : IsLocallyBoundedOn f s)
(hg : IsLocallyBoundedOn g s)
:
IsLocallyBoundedOn (fun (x : α) => f x + g x) s
theorem
IsLocallyBoundedOn.sub
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f g : α → β}
{s : Set α}
(hf : IsLocallyBoundedOn f s)
(hg : IsLocallyBoundedOn g s)
:
IsLocallyBoundedOn (fun (x : α) => f x - g x) s
theorem
IsLocallyBoundedOn.neg
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f : α → β}
{s : Set α}
(hf : IsLocallyBoundedOn f s)
:
IsLocallyBoundedOn (fun (x : α) => -f x) s
theorem
IsLocallyBoundedOn.smul
{α : Type u_1}
{β : Type u_2}
{𝕜 : Type u_3}
[TopologicalSpace α]
[SeminormedRing 𝕜]
[SeminormedAddCommGroup β]
[Module 𝕜 β]
[IsBoundedSMul 𝕜 β]
{f : α → β}
{s : Set α}
(c : 𝕜)
(hf : IsLocallyBoundedOn f s)
:
IsLocallyBoundedOn (fun (x : α) => c • f x) s
theorem
IsLocallyBoundedOn.mul
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedRing β]
{f g : α → β}
{s : Set α}
(hf : IsLocallyBoundedOn f s)
(hg : IsLocallyBoundedOn g s)
:
IsLocallyBoundedOn (fun (x : α) => f x * g x) s
theorem
IsLocallyBoundedOn.norm
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[SeminormedAddCommGroup β]
{f : α → β}
{s : Set α}
(hf : IsLocallyBoundedOn f s)
:
IsLocallyBoundedOn (fun (x : α) => ‖f x‖) s
theorem
IsLocallyBounded.isLocallyBoundedOn
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[Norm β]
{f : α → β}
(s : Set α)
(hf : IsLocallyBounded f)
: