Extension of set functions to integrable functions

This file defines MeasureTheory.setToFun, the function-level version of MeasureTheory.L1.setToL1. It applies the L¹ extension to an integrable function and is defined to be zero when the function is not integrable or the target is not complete.

The file proves the core algebraic, congruence, order, indicator, simple-function, and continuity properties of setToFun, including continuity under convergence in L¹.

noncomputable def MeasureTheory.setToFun {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} (μ : Measure α) (T : Set α → E →L[ℝ] F) {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : F

Extend T : Set α → E →L[ℝ] F to (α → E) → F (for integrable functions α → E). We set it to 0 if the function is not integrable or if the target space is not complete.

Equations

• MeasureTheory.setToFun μ T hT f = if _hF : CompleteSpace F then if hf : MeasureTheory.Integrable f μ then (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf) else 0 else 0

theorem MeasureTheory.setToFun_eq {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} [hF : CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) : setToFun μ T hT f = (L1.setToL1 hT) (Integrable.toL1 f hf)

theorem MeasureTheory.L1.setToFun_eq_setToL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C) (f : ↥(Lp E 1 μ)) : setToFun μ T hT ↑↑f = (setToL1 hT) f

theorem MeasureTheory.setToFun_undef {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : ¬Integrable f μ) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_non_aestronglyMeasurable {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : ¬AEStronglyMeasurable f μ) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_congr_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : α → E) : setToFun μ T hT f = setToFun μ T' hT' f

theorem MeasureTheory.setToFun_congr_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) (f : α → E) : setToFun μ T hT f = setToFun μ T' hT' f

theorem MeasureTheory.setToFun_add_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (f : α → E) : setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

theorem MeasureTheory.setToFun_add_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hT'' : DominatedFinMeasAdditive μ T'' C'') (h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) (f : α → E) : setToFun μ T'' hT'' f = setToFun μ T hT f + setToFun μ T' hT' f

setToFun applied to the sum T + T' of two operators is the sum of the corresponding setToFun. See also setToFun_add_left' for a version varying the reference measures.

theorem MeasureTheory.setToFun_smul_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : α → E) : setToFun μ (fun (s : Set α) => c • T s) ⋯ f = c • setToFun μ T hT f

theorem MeasureTheory.setToFun_smul_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (c : ℝ) (h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) (f : α → E) : setToFun μ T' hT' f = c • setToFun μ T hT f

@[simp]

theorem MeasureTheory.setToFun_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : setToFun μ T hT 0 = 0

@[simp]

theorem MeasureTheory.setToFun_zero_left {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {C : ℝ} {f : α → E} {hT : DominatedFinMeasAdditive μ 0 C} : setToFun μ 0 hT f = 0

theorem MeasureTheory.setToFun_zero_left' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (h_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = 0) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hg : Integrable g μ) : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

theorem MeasureTheory.setToFun_finsetSum' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {ι : Type u_5} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

@[deprecated MeasureTheory.setToFun_finsetSum' (since := "2026-04-08")]

theorem MeasureTheory.setToFun_finset_sum' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {ι : Type u_5} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)

Alias of MeasureTheory.setToFun_finsetSum'.

theorem MeasureTheory.setToFun_finsetSum {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {ι : Type u_5} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : (setToFun μ T hT fun (a : α) => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)

@[deprecated MeasureTheory.setToFun_finsetSum (since := "2026-04-08")]

theorem MeasureTheory.setToFun_finset_sum {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {ι : Type u_5} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, Integrable (f i) μ) : (setToFun μ T hT fun (a : α) => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)

Alias of MeasureTheory.setToFun_finsetSum.

theorem MeasureTheory.setToFun_neg {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : setToFun μ T hT (-f) = -setToFun μ T hT f

theorem MeasureTheory.setToFun_neg' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (f : α → E) : setToFun μ (-T) ⋯ f = -setToFun μ T hT f

theorem MeasureTheory.setToFun_sub {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) (hg : Integrable g μ) : setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g

theorem MeasureTheory.setToFun_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [Module 𝕜 F] [NormSMulClass 𝕜 F] (hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x) (c : 𝕜) (f : α → E) : setToFun μ T hT (c • f) = c • setToFun μ T hT f

theorem MeasureTheory.setToFun_congr_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E} (hT : DominatedFinMeasAdditive μ T C) (h : f =ᵐ[μ] g) : setToFun μ T hT f = setToFun μ T hT g

theorem MeasureTheory.setToFun_measure_zero {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (h : μ = 0) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_measure_zero' {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → μ s = 0) : setToFun μ T hT f = 0

theorem MeasureTheory.setToFun_toL1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) : setToFun μ T hT ↑↑(Integrable.toL1 f hf) = setToFun μ T hT f

theorem MeasureTheory.setToFun_indicator_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E) : setToFun μ T hT (s.indicator fun (x_1 : α) => x) = (T s) x

theorem MeasureTheory.setToFun_const {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] [IsFiniteMeasure μ] (hT : DominatedFinMeasAdditive μ T C) (x : E) : (setToFun μ T hT fun (x_1 : α) => x) = (T Set.univ) x

theorem MeasureTheory.setToFun_simpleFunc {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) : setToFun μ T hT ⇑f = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x

theorem MeasureTheory.setToFun_simpleFunc_eq_setToSimpleFunc {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] (hT : DominatedFinMeasAdditive μ T C) (f : SimpleFunc α E) (hf : Integrable (⇑f) μ) : setToFun μ T hT ⇑f = SimpleFunc.setToSimpleFunc T f

theorem MeasureTheory.setToFun_mono_left' {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_6} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x) (f : α → E) : setToFun μ T hT f ≤ setToFun μ T' hT' f

theorem MeasureTheory.setToFun_mono_left {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {m : MeasurableSpace α} {μ : Measure α} {G'' : Type u_6} [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [OrderClosedTopology G''] {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) (f : ↥(Lp E 1 μ)) : setToFun μ T hT ↑↑f ≤ setToFun μ T' hT' ↑↑f

theorem MeasureTheory.setToFun_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_5} {G'' : Type u_6} [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [ClosedIciTopology G''] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f : α → G'} (hf : 0 ≤ᵐ[μ] f) : 0 ≤ setToFun μ T hT f

theorem MeasureTheory.setToFun_mono {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {G' : Type u_5} {G'' : Type u_6} [NormedAddCommGroup G'] [PartialOrder G'] [NormedSpace ℝ G'] [NormedAddCommGroup G''] [PartialOrder G''] [IsOrderedAddMonoid G''] [NormedSpace ℝ G''] [ClosedIciTopology G''] [IsOrderedAddMonoid G'] {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) (hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x) {f g : α → G'} (hf : Integrable f μ) (hg : Integrable g μ) (hfg : f ≤ᵐ[μ] g) : setToFun μ T hT f ≤ setToFun μ T hT g

theorem MeasureTheory.continuous_setToFun {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) : Continuous fun (f : ↥(Lp E 1 μ)) => setToFun μ T hT ↑↑f

theorem MeasureTheory.tendsto_setToFun_of_L1 {α : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {m : MeasurableSpace α} {μ : Measure α} {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C) {ι : Type u_5} (f : α → E) (hf : AEStronglyMeasurable f μ) {fs : ι → α → E} {l : Filter ι} (hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ) (hfs : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => setToFun μ T hT (fs i)) l (nhds (setToFun μ T hT f))

If F i → f in L1, then setToFun μ T hT (F i) → setToFun μ T hT f.