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.induction'' {α : Type u_1} [MeasurableSpace α] {motive : SimpleFunc α NNReal → Prop} (const : ∀ (c : NNReal) {s : Set α}, MeasurableSet s → motive ((const α c).restrict s)) (add : ∀ ⦃f : SimpleFunc α NNReal⦄ (c : NNReal) ⦃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 α NNReal) : 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 : ℕ} : (approx i f n) a ≤ f a

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 = ⊥) : ⨆ (n : ℕ), (approx i f n) a = ⨆ (k : ℕ), ⨆ (_ : i k ≤ f a), i k

def MeasureTheory.SimpleFunc.nnrealRatEmbed (n : ℕ) : NNReal

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

theorem MeasureTheory.SimpleFunc.nnrealRatEmbed_encode (q : ℚ) : nnrealRatEmbed (Encodable.encode q) = (↑q).toNNReal

def MeasureTheory.SimpleFunc.nnapprox {α : Type u_1} [MeasurableSpace α] : (α → NNReal) → ℕ → SimpleFunc α NNReal

Approximate a function α → ℝ≥0 by a sequence of simple functions.

Equations

• MeasureTheory.SimpleFunc.nnapprox = MeasureTheory.SimpleFunc.approx MeasureTheory.SimpleFunc.nnrealRatEmbed

theorem MeasureTheory.SimpleFunc.monotone_nnapprox {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} : Monotone (nnapprox f)

theorem MeasureTheory.SimpleFunc.iSup_nnapprox_apply {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} (hf : Measurable f) (a : α) : ⨆ (n : ℕ), (nnapprox f n) a = f a

theorem MeasureTheory.SimpleFunc.iSup_nnapprox {α : Type u_1} [MeasurableSpace α] {f : α → NNReal} (hf : Measurable f) : (fun (a : α) => ⨆ (n : ℕ), (nnapprox f n) a) = 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