theorem
MeasureTheory.SimpleFunc.measurable_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
{f : SimpleFunc α β}
{g : β → γ}
:
Measurable (g ∘ ⇑f)
theorem
MeasureTheory.SimpleFunc.measurable_comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
{f : SimpleFunc α β}
{g : β → γ}
:
Measurable fun (a : α) => g (f a)
theorem
MeasureTheory.SimpleFunc.induction₀
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[AddZeroClass γ]
{motive : SimpleFunc α γ → Prop}
(const : ∀ (c : γ) {s : Set α}, MeasurableSet s → motive ((const α c).restrict s))
(add :
∀ ⦃f : SimpleFunc α γ⦄ (c : γ) ⦃s : Set α⦄,
MeasurableSet s →
Disjoint (Function.support ⇑f) s →
motive f → motive ((SimpleFunc.const α c).restrict s) → motive (f + (SimpleFunc.const α c).restrict s))
(f : SimpleFunc α γ)
:
motive f
theorem
MeasureTheory.SimpleFunc.Antitone.support_eq
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrderBot α]
[AddMonoid β]
[LinearOrder β]
[CanonicallyOrderedAdd β]
[OrderBot β]
{f : α → β}
(hf : Antitone f)
:
Function.support f = if BddAbove (Function.support f) then
if sSup (Function.support f) ∈ Function.support f then Set.Iic (sSup (Function.support f))
else Set.Iio (sSup (Function.support f))
else Set.univ
theorem
MeasureTheory.SimpleFunc.antitone_induction
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[ConditionallyCompleteLinearOrderBot α]
[LinearOrder β]
[AddCommMonoid β]
[CanonicallyOrderedAdd β]
[OrderBot β]
[Sub β]
[OrderedSub β]
{motive : SimpleFunc α β → Prop}
(const'' : ∀ (c : β) (b : α), motive ((const α c).restrict (Set.Iio b)))
(const' : ∀ (c : β) (b : α), motive ((const α c).restrict (Set.Iic b)))
(const : ∀ (c : β), motive (const α c))
(add :
∀ ⦃f : SimpleFunc α β⦄ (c : β) ⦃s : Set α⦄,
MeasurableSet s →
Function.support ⇑f ⊆ s →
motive f → motive ((SimpleFunc.const α c).restrict s) → motive (f + (SimpleFunc.const α c).restrict s))
(f : SimpleFunc α β)
(hf : Antitone ⇑f)
:
motive f
theorem
MeasureTheory.SimpleFunc.induction''
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[LinearOrder β]
[AddCommMonoid β]
[CanonicallyOrderedAdd β]
[OrderBot β]
[Sub β]
[OrderedSub β]
{motive : SimpleFunc α β → Prop}
(const : ∀ (c : β) {s : Set α}, MeasurableSet s → motive ((const α c).restrict s))
(add :
∀ ⦃f : SimpleFunc α β⦄ (c : β) ⦃s : Set α⦄,
MeasurableSet s →
Function.support ⇑f ⊆ s →
motive f → motive ((SimpleFunc.const α c).restrict s) → motive (f + (SimpleFunc.const α c).restrict s))
(f : SimpleFunc α β)
:
motive f
theorem
MeasureTheory.SimpleFunc.approx_le
{α : Type u_1}
{β : Type u_2}
[inst : MeasurableSpace α]
[ConditionallyCompleteLinearOrderBot β]
[Zero β]
[TopologicalSpace β]
[OrderClosedTopology β]
[MeasurableSpace β]
[OpensMeasurableSpace β]
{i : ℕ → β}
{f : α → β}
(hf : Measurable f)
(h_zero : 0 = ⊥)
{a : α}
{n : ℕ}
:
theorem
MeasureTheory.SimpleFunc.iSup_approx_apply'
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[ConditionallyCompleteLinearOrderBot β]
[TopologicalSpace β]
[OrderClosedTopology β]
[Zero β]
[MeasurableSpace β]
[OpensMeasurableSpace β]
(i : ℕ → β)
(f : α → β)
(a : α)
(hf : Measurable f)
(h_zero : 0 = ⊥)
:
A sequence of ℝ≥0s such that its range is the set of non-negative rational numbers.
Equations
- MeasureTheory.SimpleFunc.nnrealRatEmbed n = (↑((Encodable.decode n).getD 0)).toNNReal
Instances For
noncomputable def
MeasureTheory.SimpleFunc.nnapprox
{α : Type u_1}
[MeasurableSpace α]
:
(α → NNReal) → ℕ → SimpleFunc α NNReal
Approximate a function α → ℝ≥0 by a sequence of simple functions.
Equations
Instances For
theorem
MeasureTheory.SimpleFunc.nnapprox_le
{α : Type u_1}
[MeasurableSpace α]
{f : α → NNReal}
(hf : Measurable f)
{a : α}
{n : ℕ}
:
theorem
MeasureTheory.SimpleFunc.monotone_nnapprox
{α : Type u_1}
[MeasurableSpace α]
{f : α → NNReal}
:
theorem
MeasureTheory.SimpleFunc.iSup_nnapprox_apply
{α : Type u_1}
[MeasurableSpace α]
{f : α → NNReal}
(hf : Measurable f)
(a : α)
:
theorem
MeasureTheory.SimpleFunc.iSup_nnapprox
{α : Type u_1}
[MeasurableSpace α]
{f : α → NNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.Measurable.nnreal_induction
{α : Type u_5}
{mα : MeasurableSpace α}
{motive : (α → NNReal) → Prop}
(simpleFunc : ∀ ⦃f : SimpleFunc α NNReal⦄, motive ⇑f)
(approx : ∀ ⦃f : α → NNReal⦄, Measurable f → (∀ (n : ℕ), motive ⇑(SimpleFunc.nnapprox f n)) → motive f)
⦃f : α → NNReal⦄
(hf : Measurable f)
:
motive f
modelled after Measurable.ennreal_induction but with very raw assumptions
theorem
MeasureTheory.Measurable.ennreal_induction'
{α : Type u_5}
{mα : MeasurableSpace α}
{motive : (α → ENNReal) → Prop}
(simpleFunc : ∀ ⦃f : SimpleFunc α ENNReal⦄, motive ⇑f)
(iSup :
∀ ⦃f : ℕ → SimpleFunc α ENNReal⦄, Monotone f → (∀ (n : ℕ), motive ⇑(f n)) → motive fun (x : α) => ⨆ (n : ℕ), (f n) x)
⦃f : α → ENNReal⦄
(hf : Measurable f)
:
motive f
theorem
MeasureTheory.Antitone.antitone_eapprox
{α : Type u_5}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
[LinearOrder α]
[OrderClosedTopology α]
⦃f : α → ENNReal⦄
(hf : Antitone f)
{n : ℕ}
:
Antitone ⇑(SimpleFunc.eapprox f n)
theorem
MeasureTheory.Antitone.ennreal_induction'
{α : Type u_5}
[TopologicalSpace α]
{mα : MeasurableSpace α}
[BorelSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{motive : (α → ENNReal) → Prop}
(simpleFunc : ∀ ⦃f : SimpleFunc α ENNReal⦄, Antitone ⇑f → motive ⇑f)
(iSup :
∀ ⦃f : ℕ → SimpleFunc α ENNReal⦄, Monotone f → (∀ (n : ℕ), motive ⇑(f n)) → motive fun (x : α) => ⨆ (n : ℕ), (f n) x)
⦃f : α → ENNReal⦄
(hf : Antitone f)
:
motive f