9.2. フビニの定理🔗

X と Y を可測空間とし、\mu を X 上の測度、\nu を Y 上の測度とします。

補題.

f : X \times Y \to \mathbb{R} が \mu \times \nu に関して可積分であるとする。 \nu は S-有限であると仮定する。このとき \mu-ほとんど至る所の x \in X に対して、部分適用 f (x, -) : Y \to \mathbb{R} は \nu に関して可積分である。

Lean code

/-- Almost every section of an integrable function is integrable. -/
theorem ae_integrable_sections [SFinite ν] {f : X × Y → ℝ}
    (hf : Integrable f (μ.prod ν)) :
    ∀ᵐ x ∂μ, Integrable (fun y ↦ f (x, y)) ν := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
  let Gpos : X → ℝ≥0∞ := fun x ↦ ∫⁻ y, posPart f (x, y) ∂νX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂ν⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
  let Gneg : X → ℝ≥0∞ := fun x ↦ ∫⁻ y, negPart f (x, y) ∂νX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂ν⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
  have hpos_meas : Measurable (posPart f) := measurable_posPart hf.measurableX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurable⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
  have hneg_meas : Measurable (negPart f) := measurable_negPart hf.measurableX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurable⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
  have hGpos_meas : Measurable Gpos := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa [Gpos] using hpos_meas.lintegral_prod_right'All goals completed! 🐙
  have hGneg_meas : Measurable Gneg := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa [Gneg] using hneg_meas.lintegral_prod_right'All goals completed! 🐙
  have hGpos_eq :
      ∫⁻ x, Gpos x ∂μ = ∫⁻ z, posPart f z ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa [Gpos] using (lintegral_prod hpos_meas).symmAll goals completed! 🐙
  have hGneg_eq :
      ∫⁻ x, Gneg x ∂μ = ∫⁻ z, negPart f z ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa [Gneg] using (lintegral_prod hneg_meas).symmAll goals completed! 🐙
  have hGpos_fin_ae : ∀ᵐ x ∂μ, Gpos x < ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    apply ae_lt_top hGpos_measX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))⊢ ∫⁻ (x : X), Gpos x ∂μ ≠ ∞
    rw [hGpos_eq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))⊢ ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν ≠ ∞
    exact hf.hasFiniteIntegral.pos_ne_topAll goals completed! 🐙
  have hGneg_fin_ae : ∀ᵐ x ∂μ, Gneg x < ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    apply ae_lt_top hGneg_measX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))⊢ ∫⁻ (x : X), Gneg x ∂μ ≠ ∞
    rw [hGneg_eq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))⊢ ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν ≠ ∞
    exact hf.hasFiniteIntegral.neg_ne_topAll goals completed! 🐙
  filter_upwards [hGpos_fin_ae, hGneg_fin_ae] with x hxposhX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := 
  ae_lt_top hGneg_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral))x:Xhxpos:Gpos x < ∞⊢ Gneg x < ∞ → Integrable (fun y => f (x, y)) ν hxneghX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := 
  ae_lt_top hGneg_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral))x:Xhxpos:Gpos x < ∞hxneg:Gneg x < ∞⊢ Integrable (fun y => f (x, y)) ν
  have hsec_meas : Measurable fun y ↦ f (x, y) := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa using hf.measurable.comp (measurable_prodMk_left (x := x))All goals completed! 🐙
  have hsec_pos_meas : Measurable fun y ↦ posPart (fun y ↦ f (x, y)) y := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    exact measurable_posPart hsec_measAll goals completed! 🐙
  have hsec_pos_fin : ∫⁻ y, posPart (fun y ↦ f (x, y)) y ∂ν ≠ ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa [Gpos, posPart] using hxpos.neAll goals completed! 🐙
  have hsec_neg_fin : ∫⁻ y, negPart (fun y ↦ f (x, y)) y ∂ν ≠ ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∀ᵐ (x : X) ∂μ, Integrable (fun y => f (x, y)) ν
    simpa [Gneg, negPart] using hxneg.neAll goals completed! 🐙
  refine ⟨hsec_meas, ?_⟩hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := 
  ae_lt_top hGneg_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral))x:Xhxpos:Gpos x < ∞hxneg:Gneg x < ∞hsec_meas:Measurable fun y => f (x, y) := Measurable.comp hf.measurable measurable_prodMk_lefthsec_pos_meas:Measurable fun y => posPart (fun y => f (x, y)) y := measurable_posPart hsec_meashsec_pos_fin:∫⁻ (y : Y), posPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxpos)hsec_neg_fin:∫⁻ (y : Y), negPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxneg)⊢ HasFiniteIntegral (fun y => f (x, y)) ν
  refine hasFiniteIntegral_of_ne_top ?_hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := 
  ae_lt_top hGneg_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral))x:Xhxpos:Gpos x < ∞hxneg:Gneg x < ∞hsec_meas:Measurable fun y => f (x, y) := Measurable.comp hf.measurable measurable_prodMk_lefthsec_pos_meas:Measurable fun y => posPart (fun y => f (x, y)) y := measurable_posPart hsec_meashsec_pos_fin:∫⁻ (y : Y), posPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxpos)hsec_neg_fin:∫⁻ (y : Y), negPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxneg)⊢ ∫⁻ (x_1 : Y), ENNReal.ofReal |f (x, x_1)| ∂ν ≠ ∞
  rw [show (∫⁻ y, ENNReal.ofReal |f (x, y)| ∂ν)
      = ∫⁻ y, (posPart (fun y ↦ f (x, y)) y + negPart (fun y ↦ f (x, y)) y) ∂ν by
        apply lintegral_congr
        intro y
        symm
        exact posPart_add_negPart_eq_abs (f := fun y ↦ f (x, y)) y]hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := 
  ae_lt_top hGneg_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral))x:Xhxpos:Gpos x < ∞hxneg:Gneg x < ∞hsec_meas:Measurable fun y => f (x, y) := Measurable.comp hf.measurable measurable_prodMk_lefthsec_pos_meas:Measurable fun y => posPart (fun y => f (x, y)) y := measurable_posPart hsec_meashsec_pos_fin:∫⁻ (y : Y), posPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxpos)hsec_neg_fin:∫⁻ (y : Y), negPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxneg)⊢ ∫⁻ (y : Y), posPart (fun y => f (x, y)) y + negPart (fun y => f (x, y)) y ∂ν ≠ ∞
  rw [lintegral_add_left hsec_pos_meas]hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := 
  ae_lt_top hGpos_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral))hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := 
  ae_lt_top hGneg_meas
    (Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral))x:Xhxpos:Gpos x < ∞hxneg:Gneg x < ∞hsec_meas:Measurable fun y => f (x, y) := Measurable.comp hf.measurable measurable_prodMk_lefthsec_pos_meas:Measurable fun y => posPart (fun y => f (x, y)) y := measurable_posPart hsec_meashsec_pos_fin:∫⁻ (y : Y), posPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxpos)hsec_neg_fin:∫⁻ (y : Y), negPart (fun y => f (x, y)) y ∂ν ≠ ∞ := id (LT.lt.ne hxneg)⊢ ∫⁻ (a : Y), posPart (fun y => f (x, y)) a ∂ν + ∫⁻ (a : Y), negPart (fun y => f (x, y)) a ∂ν ≠ ∞
  exact add_ne_top.mpr ⟨hsec_pos_fin, hsec_neg_fin⟩All goals completed! 🐙

補題.

f : X \times Y \to \mathbb{R} が \mu \times \nu に関して可積分であるとする。 \nu は S-有限であると仮定する。このとき関数 x \longmapsto \int_{y \in Y} f^+(x,y)\,d\nu は X から \mathbb{R} への関数として \mu に関して可積分である。

Lean code

/-- The positive-part section integral is measurable in the outer variable. -/
theorem measurable_integral_section_posPart [SFinite ν] {f : X × Y → ℝ}
    (hf_meas : Measurable f) :
    Measurable fun x ↦ ∫ y, (posPart f (x, y)).toReal ∂ν := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable f⊢ Measurable fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
  let Gpos : X → ℝ≥0∞ := fun x ↦ ∫⁻ y, posPart f (x, y) ∂νX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂ν⊢ Measurable fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
  have hpos_meas : Measurable (posPart f) := measurable_posPart hf_measX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf_meas⊢ Measurable fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
  have hGpos_meas : Measurable Gpos := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable f⊢ Measurable fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
    simpa [Gpos] using hpos_meas.lintegral_prod_right'All goals completed! 🐙
  have hEq :
      (fun x ↦ ∫ y, (posPart f (x, y)).toReal ∂ν) = fun x ↦ (Gpos x).toReal := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable f⊢ Measurable fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
    funext xhX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf_meashGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)x:X⊢ ∫ (y : Y), (posPart f (x, y)).toReal ∂ν = (Gpos x).toReal
    simpa [Gpos] using integral_section_posPart_eq_toReal_lintegral hf_meas xAll goals completed! 🐙
  rw [hEq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf_meashGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hEq:(fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν) = fun x => (Gpos x).toReal := funext fun x => id (integral_section_posPart_eq_toReal_lintegral hf_meas x)⊢ Measurable fun x => (Gpos x).toReal
  simpa using hGpos_meas.ennreal_toRealAll goals completed! 🐙

/-- The positive-part section integrals have finite lower integral. -/
theorem lintegral_integral_section_posPart_ne_top [SFinite ν] {f : X × Y → ℝ}
    (hf : Integrable f (μ.prod ν)) :
    ∫⁻ x, ENNReal.ofReal (∫ y, (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  let Gpos : X → ℝ≥0∞ := fun x ↦ ∫⁻ y, posPart f (x, y) ∂νX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂ν⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  have hpos_meas : Measurable (posPart f) := measurable_posPart hf.measurableX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurable⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  have hGpos_meas : Measurable Gpos := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    simpa [Gpos] using hpos_meas.lintegral_prod_right'All goals completed! 🐙
  have hGpos_eq :
      ∫⁻ x, Gpos x ∂μ = ∫⁻ z, posPart f z ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    simpa [Gpos] using (lintegral_prod hpos_meas).symmAll goals completed! 🐙
  have hGpos_fin : ∫⁻ x, Gpos x ∂μ ≠ ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    rw [hGpos_eq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))⊢ ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν ≠ ∞
    exact hf.hasFiniteIntegral.pos_ne_topAll goals completed! 🐙
  have hGpos_fin_ae : ∀ᵐ x ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_finX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGpos_fin:∫⁻ (x : X), Gpos x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral)hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_fin⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  have hEq :
      ∫⁻ x, ENNReal.ofReal (∫ y, (posPart f (x, y)).toReal ∂ν) ∂μ = ∫⁻ x, Gpos x ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    refine lintegral_congr_ae ?_X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGpos_fin:∫⁻ (x : X), Gpos x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral)hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_fin⊢ (fun x => ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν)) =ᶠ[ae μ] Gpos
    exact hGpos_fin_ae.mono fun x hx ↦ byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGpos_fin:∫⁻ (x : X), Gpos x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral)hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_finx:Xhx:Gpos x < ∞⊢ (fun x => ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν)) x = Gpos x
      change ENNReal.ofReal (∫ y, (posPart f (x, y)).toReal ∂ν) = Gpos xX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGpos_fin:∫⁻ (x : X), Gpos x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral)hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_finx:Xhx:Gpos x < ∞⊢ ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) = Gpos x
      rw [integral_section_posPart_eq_toReal_lintegral hf.measurable x]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGpos_fin:∫⁻ (x : X), Gpos x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral)hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_finx:Xhx:Gpos x < ∞⊢ ENNReal.ofReal (∫⁻ (y : Y), posPart f (x, y) ∂ν).toReal = Gpos x
      simpa [Gpos] using (ENNReal.ofReal_toReal hx.ne)All goals completed! 🐙
  rw [hEq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gpos:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), posPart f (x, y) ∂νhpos_meas:Measurable (posPart f) := measurable_posPart hf.measurablehGpos_meas:Measurable Gpos := id (Measurable.lintegral_prod_right' hpos_meas)hGpos_eq:∫⁻ (x : X), Gpos x ∂μ = ∫⁻ (z : X × Y), posPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hpos_meas))hGpos_fin:∫⁻ (x : X), Gpos x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGpos_eq)) (HasFiniteIntegral.pos_ne_top hf.hasFiniteIntegral)hGpos_fin_ae:∀ᵐ (x : X) ∂μ, Gpos x < ∞ := ae_lt_top hGpos_meas hGpos_finhEq:∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ = ∫⁻ (x : X), Gpos x ∂μ := 
  lintegral_congr_ae
    (Filter.Eventually.mono hGpos_fin_ae fun x hx =>
      id
        (Eq.mpr
          (id
            (congrArg (fun _a => ENNReal.ofReal _a = Gpos x)
              (integral_section_posPart_eq_toReal_lintegral hf.measurable x)))
          (Eq.mpr (id ofReal_toReal_eq_iff._simp_1) (Eq.mp ofReal_toReal_eq_iff._simp_1 (ofReal_toReal (LT.lt.ne hx))))))⊢ ∫⁻ (x : X), Gpos x ∂μ ≠ ∞
  exact hGpos_finAll goals completed! 🐙

/-- The positive-part section integrals are integrable in the outer variable. -/
theorem integrable_integral_section_posPart [SFinite ν] {f : X × Y → ℝ}
    (hf : Integrable f (μ.prod ν)) :
    Integrable (fun x ↦ ∫ y, (posPart f (x, y)).toReal ∂ν) μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ Integrable (fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν) μ
  refine ⟨measurable_integral_section_posPart hf.measurable, ?_⟩X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ HasFiniteIntegral (fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν) μ
  refine hasFiniteIntegral_of_ne_top ?_X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal |∫ (y : Y), (posPart f (x, y)).toReal ∂ν| ∂μ ≠ ∞
  have hEq :
      ∫⁻ x, ENNReal.ofReal |∫ y, (posPart f (x, y)).toReal ∂ν| ∂μ
        = ∫⁻ x, ENNReal.ofReal (∫ y, (posPart f (x, y)).toReal ∂ν) ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ Integrable (fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν) μ
    refine lintegral_congr fun x ↦ ?_X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ ENNReal.ofReal |∫ (y : Y), (posPart f (x, y)).toReal ∂ν| = ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν)
    congr 1e_rX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ |∫ (y : Y), (posPart f (x, y)).toReal ∂ν| = ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
    apply abs_of_nonnege_r.hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ 0 ≤ ∫ (y : Y), (posPart f (x, y)).toReal ∂ν
    rw [integral_section_posPart_eq_toReal_lintegral hf.measurable x]e_r.hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ 0 ≤ (∫⁻ (y : Y), posPart f (x, y) ∂ν).toReal
    exact ENNReal.toReal_nonnegAll goals completed! 🐙
  rw [hEq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)hEq:∫⁻ (x : X), ENNReal.ofReal |∫ (y : Y), (posPart f (x, y)).toReal ∂ν| ∂μ =
  ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ := 
  lintegral_congr fun x =>
    (fun r r_1 e_r => e_r ▸ Eq.refl (ENNReal.ofReal r)) |∫ (y : Y), (posPart f (x, y)).toReal ∂ν|
      (∫ (y : Y), (posPart f (x, y)).toReal ∂ν)
      (abs_of_nonneg
        (Eq.mpr (id (congrArg (fun _a => 0 ≤ _a) (integral_section_posPart_eq_toReal_lintegral hf.measurable x)))
          toReal_nonneg))⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (posPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  exact lintegral_integral_section_posPart_ne_top hfAll goals completed! 🐙

補題.

f : X \times Y \to \mathbb{R} が \mu \times \nu に関して可積分であるとする。 \nu は S-有限であると仮定する。このとき関数 x \longmapsto \int_{y \in Y} f^-(x,y)\,d\nu は X から \mathbb{R} への関数として \mu に関して可積分である。

Lean code

/-- The negative-part section integral is measurable in the outer variable. -/
theorem measurable_integral_section_negPart [SFinite ν] {f : X × Y → ℝ}
    (hf_meas : Measurable f) :
    Measurable fun x ↦ ∫ y, (negPart f (x, y)).toReal ∂ν := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable f⊢ Measurable fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
  let Gneg : X → ℝ≥0∞ := fun x ↦ ∫⁻ y, negPart f (x, y) ∂νX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂ν⊢ Measurable fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
  have hneg_meas : Measurable (negPart f) := measurable_negPart hf_measX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf_meas⊢ Measurable fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
  have hGneg_meas : Measurable Gneg := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable f⊢ Measurable fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
    simpa [Gneg] using hneg_meas.lintegral_prod_right'All goals completed! 🐙
  have hEq :
      (fun x ↦ ∫ y, (negPart f (x, y)).toReal ∂ν) = fun x ↦ (Gneg x).toReal := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable f⊢ Measurable fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
    funext xhX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf_meashGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)x:X⊢ ∫ (y : Y), (negPart f (x, y)).toReal ∂ν = (Gneg x).toReal
    simpa [Gneg] using integral_section_negPart_eq_toReal_lintegral hf_meas xAll goals completed! 🐙
  rw [hEq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yν:Measure Yinst✝:SFinite νf:X × Y → ℝhf_meas:Measurable fGneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf_meashGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hEq:(fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν) = fun x => (Gneg x).toReal := funext fun x => id (integral_section_negPart_eq_toReal_lintegral hf_meas x)⊢ Measurable fun x => (Gneg x).toReal
  simpa using hGneg_meas.ennreal_toRealAll goals completed! 🐙

/-- The negative-part section integrals have finite lower integral. -/
theorem lintegral_integral_section_negPart_ne_top [SFinite ν] {f : X × Y → ℝ}
    (hf : Integrable f (μ.prod ν)) :
    ∫⁻ x, ENNReal.ofReal (∫ y, (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  let Gneg : X → ℝ≥0∞ := fun x ↦ ∫⁻ y, negPart f (x, y) ∂νX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂ν⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  have hneg_meas : Measurable (negPart f) := measurable_negPart hf.measurableX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurable⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  have hGneg_meas : Measurable Gneg := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    simpa [Gneg] using hneg_meas.lintegral_prod_right'All goals completed! 🐙
  have hGneg_eq :
      ∫⁻ x, Gneg x ∂μ = ∫⁻ z, negPart f z ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    simpa [Gneg] using (lintegral_prod hneg_meas).symmAll goals completed! 🐙
  have hGneg_fin : ∫⁻ x, Gneg x ∂μ ≠ ∞ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    rw [hGneg_eq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))⊢ ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν ≠ ∞
    exact hf.hasFiniteIntegral.neg_ne_topAll goals completed! 🐙
  have hGneg_fin_ae : ∀ᵐ x ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_finX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGneg_fin:∫⁻ (x : X), Gneg x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral)hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_fin⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  have hEq :
      ∫⁻ x, ENNReal.ofReal (∫ y, (negPart f (x, y)).toReal ∂ν) ∂μ = ∫⁻ x, Gneg x ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
    refine lintegral_congr_ae ?_X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGneg_fin:∫⁻ (x : X), Gneg x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral)hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_fin⊢ (fun x => ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν)) =ᶠ[ae μ] Gneg
    exact hGneg_fin_ae.mono fun x hx ↦ byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGneg_fin:∫⁻ (x : X), Gneg x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral)hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_finx:Xhx:Gneg x < ∞⊢ (fun x => ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν)) x = Gneg x
      change ENNReal.ofReal (∫ y, (negPart f (x, y)).toReal ∂ν) = Gneg xX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGneg_fin:∫⁻ (x : X), Gneg x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral)hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_finx:Xhx:Gneg x < ∞⊢ ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) = Gneg x
      rw [integral_section_negPart_eq_toReal_lintegral hf.measurable x]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGneg_fin:∫⁻ (x : X), Gneg x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral)hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_finx:Xhx:Gneg x < ∞⊢ ENNReal.ofReal (∫⁻ (y : Y), negPart f (x, y) ∂ν).toReal = Gneg x
      simpa [Gneg] using (ENNReal.ofReal_toReal hx.ne)All goals completed! 🐙
  rw [hEq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)Gneg:X → ℝ≥0∞ := fun x => ∫⁻ (y : Y), negPart f (x, y) ∂νhneg_meas:Measurable (negPart f) := measurable_negPart hf.measurablehGneg_meas:Measurable Gneg := id (Measurable.lintegral_prod_right' hneg_meas)hGneg_eq:∫⁻ (x : X), Gneg x ∂μ = ∫⁻ (z : X × Y), negPart f z ∂μ.prod ν := id (Eq.symm (lintegral_prod hneg_meas))hGneg_fin:∫⁻ (x : X), Gneg x ∂μ ≠ ∞ := Eq.mpr (id (congrArg (fun _a => _a ≠ ∞) hGneg_eq)) (HasFiniteIntegral.neg_ne_top hf.hasFiniteIntegral)hGneg_fin_ae:∀ᵐ (x : X) ∂μ, Gneg x < ∞ := ae_lt_top hGneg_meas hGneg_finhEq:∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ = ∫⁻ (x : X), Gneg x ∂μ := 
  lintegral_congr_ae
    (Filter.Eventually.mono hGneg_fin_ae fun x hx =>
      id
        (Eq.mpr
          (id
            (congrArg (fun _a => ENNReal.ofReal _a = Gneg x)
              (integral_section_negPart_eq_toReal_lintegral hf.measurable x)))
          (Eq.mpr (id ofReal_toReal_eq_iff._simp_1) (Eq.mp ofReal_toReal_eq_iff._simp_1 (ofReal_toReal (LT.lt.ne hx))))))⊢ ∫⁻ (x : X), Gneg x ∂μ ≠ ∞
  exact hGneg_finAll goals completed! 🐙

/-- The negative-part section integrals are integrable in the outer variable. -/
theorem integrable_integral_section_negPart [SFinite ν] {f : X × Y → ℝ}
    (hf : Integrable f (μ.prod ν)) :
    Integrable (fun x ↦ ∫ y, (negPart f (x, y)).toReal ∂ν) μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ Integrable (fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν) μ
  refine ⟨measurable_integral_section_negPart hf.measurable, ?_⟩X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ HasFiniteIntegral (fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν) μ
  refine hasFiniteIntegral_of_ne_top ?_X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫⁻ (x : X), ENNReal.ofReal |∫ (y : Y), (negPart f (x, y)).toReal ∂ν| ∂μ ≠ ∞
  have hEq :
      ∫⁻ x, ENNReal.ofReal |∫ y, (negPart f (x, y)).toReal ∂ν| ∂μ
        = ∫⁻ x, ENNReal.ofReal (∫ y, (negPart f (x, y)).toReal ∂ν) ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ Integrable (fun x => ∫ (y : Y), (negPart f (x, y)).toReal ∂ν) μ
    refine lintegral_congr fun x ↦ ?_X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ ENNReal.ofReal |∫ (y : Y), (negPart f (x, y)).toReal ∂ν| = ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν)
    congr 1e_rX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ |∫ (y : Y), (negPart f (x, y)).toReal ∂ν| = ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
    apply abs_of_nonnege_r.hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ 0 ≤ ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
    rw [integral_section_negPart_eq_toReal_lintegral hf.measurable x]e_r.hX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:X⊢ 0 ≤ (∫⁻ (y : Y), negPart f (x, y) ∂ν).toReal
    exact ENNReal.toReal_nonnegAll goals completed! 🐙
  rw [hEq]X:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)hEq:∫⁻ (x : X), ENNReal.ofReal |∫ (y : Y), (negPart f (x, y)).toReal ∂ν| ∂μ =
  ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ := 
  lintegral_congr fun x =>
    (fun r r_1 e_r => e_r ▸ Eq.refl (ENNReal.ofReal r)) |∫ (y : Y), (negPart f (x, y)).toReal ∂ν|
      (∫ (y : Y), (negPart f (x, y)).toReal ∂ν)
      (abs_of_nonneg
        (Eq.mpr (id (congrArg (fun _a => 0 ≤ _a) (integral_section_negPart_eq_toReal_lintegral hf.measurable x)))
          toReal_nonneg))⊢ ∫⁻ (x : X), ENNReal.ofReal (∫ (y : Y), (negPart f (x, y)).toReal ∂ν) ∂μ ≠ ∞
  apply lintegral_integral_section_negPart_ne_top hfAll goals completed! 🐙

補題.

f : X \times Y \to \mathbb{R} が \mu \times \nu に関して可積分であるとする。 \nu は S-有限であると仮定する。このとき \mu-ほとんど至る所の x \in X に対して \int_{y \in Y} f(x,y)\,d\nu = \int_{y \in Y} f^+(x,y)\,d\nu - \int_{y \in Y} f^-(x,y)\,d\nu. が成り立つ。

Lean code

/-- Almost every section integral splits into the difference of the positive and negative section
integrals. -/
theorem integral_sections_eq_integral_posPart_sub_integral_negPart_ae [SFinite ν]
    {f : X × Y → ℝ} (hf : Integrable f (μ.prod ν)) :
    (fun x ↦ ∫ y, f (x, y) ∂ν) =ᵐ[μ]
      fun x ↦ ∫ y, (posPart f (x, y)).toReal ∂ν - ∫ y, (negPart f (x, y)).toReal ∂ν := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ (fun x => ∫ (y : Y), f (x, y) ∂ν) =ᶠ[ae μ] fun x =>
  ∫ (y : Y), (posPart f (x, y)).toReal ∂ν - ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
  filter_upwards [ae_integrable_sections hf] with x hxhX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)x:Xhx:Integrable (fun y => f (x, y)) ν⊢ ∫ (y : Y), f (x, y) ∂ν = ∫ (y : Y), (posPart f (x, y)).toReal ∂ν - ∫ (y : Y), (negPart f (x, y)).toReal ∂ν
  apply integral_eq_integral_posPart_sub_integral_negPart hxAll goals completed! 🐙

定理 (フビニの定理).

f : X \times Y \to \mathbb{R} が \mu \times \nu に関して可積分であるとする。 \nu は S-有限であると仮定する。このとき \int_{(x,y) \in X \times Y} f(x,y)\,d(\mu \times \nu) = \int_{x \in X} \int_{y \in Y} f(x,y)\,d\nu\,d\mu. が成り立つ。

Lean code

/-- Fubini's theorem for real-valued functions. -/
theorem integral_prod [SFinite ν] {f : X × Y → ℝ} (hf : Integrable f (μ.prod ν)) :
    ∫ p, f p ∂(μ.prod ν) = ∫ x, ∫ y, f (x, y) ∂ν ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (p : X × Y), f p ∂μ.prod ν = ∫ (x : X), ∫ (y : Y), f (x, y) ∂ν ∂μ
  calc
    ∫ p, f p ∂(μ.prod ν)
      = ∫ p, (posPart f p).toReal ∂(μ.prod ν) - ∫ p, (negPart f p).toReal ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (p : X × Y), f p ∂μ.prod ν =
  ∫ (p : X × Y), (posPart f p).toReal ∂μ.prod ν - ∫ (p : X × Y), (negPart f p).toReal ∂μ.prod ν
          apply integral_eq_integral_posPart_sub_integral_negPart hfAll goals completed! 🐙
    _ = ∫ x, ∫ y, (posPart f (x, y)).toReal ∂ν ∂μ
        - ∫ x, ∫ y, (negPart f (x, y)).toReal ∂ν ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (p : X × Y), (posPart f p).toReal ∂μ.prod ν - ∫ (p : X × Y), (negPart f p).toReal ∂μ.prod ν =
  ∫ (x : X), ∫ (y : Y), (posPart f (x, y)).toReal ∂ν ∂μ - ∫ (x : X), ∫ (y : Y), (negPart f (x, y)).toReal ∂ν ∂μ
          rw [integral_prod_posPart hf, integral_prod_negPart hf]All goals completed! 🐙
    _ = ∫ x,
          (∫ y, (posPart f (x, y)).toReal ∂ν - ∫ y, (negPart f (x, y)).toReal ∂ν) ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (x : X), ∫ (y : Y), (posPart f (x, y)).toReal ∂ν ∂μ - ∫ (x : X), ∫ (y : Y), (negPart f (x, y)).toReal ∂ν ∂μ =
  ∫ (x : X), ∫ (y : Y), (posPart f (x, y)).toReal ∂ν - ∫ (y : Y), (negPart f (x, y)).toReal ∂ν ∂μ
          symmX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (x : X), ∫ (y : Y), (posPart f (x, y)).toReal ∂ν - ∫ (y : Y), (negPart f (x, y)).toReal ∂ν ∂μ =
  ∫ (x : X), ∫ (y : Y), (posPart f (x, y)).toReal ∂ν ∂μ - ∫ (x : X), ∫ (y : Y), (negPart f (x, y)).toReal ∂ν ∂μ
          apply integral_sub_eq_integral_sub
            (integrable_integral_section_posPart hf) (integrable_integral_section_negPart hf)All goals completed! 🐙
    _ = ∫ x, ∫ y, f (x, y) ∂ν ∂μ := byX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (x : X), ∫ (y : Y), (posPart f (x, y)).toReal ∂ν - ∫ (y : Y), (negPart f (x, y)).toReal ∂ν ∂μ =
  ∫ (x : X), ∫ (y : Y), f (x, y) ∂ν ∂μ
          apply integral_congr_aehfgX:Type u_1Y:Type u_2inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ (fun x => ∫ (y : Y), (posPart f (x, y)).toReal ∂ν - ∫ (y : Y), (negPart f (x, y)).toReal ∂ν) =ᶠ[ae μ] fun x =>
  ∫ (y : Y), f (x, y) ∂ν
          apply
            (integral_sections_eq_integral_posPart_sub_integral_negPart_ae hf).symmAll goals completed! 🐙

補題.

f : X \times Y \to \mathbb{R} を可測とする。 \mu と \nu が S-有限であると仮定する。このとき \int_{(y,x) \in Y \times X} f(x,y)\,d(\nu \times \mu) = \int_{(x,y) \in X \times Y} f(x,y)\,d(\mu \times \nu). が成り立つ。

Lean code

theorem integral_prod_swap [SFinite μ] [SFinite ν] (f : X × Y → ℝ)
    (hf : Measurable f) :
    ∫ z, f z.swap ∂(ν.prod μ) = ∫ z, f z ∂(μ.prod ν) :=
  calc
    ∫ z, f z.swap ∂(ν.prod μ) = ∫ z, f z ∂(MeasureTheory.Measure.map Prod.swap (ν.prod μ)) :=
      (integral_map hf measurable_swap).symm
    _ = ∫ z, f z ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝³:MeasurableSpace Xinst✝²:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝¹:SFinite μinst✝:SFinite νf:X × Y → ℝhf:Measurable f⊢ ∫ (z : X × Y), f z ∂map Prod.swap (ν.prod μ) = ∫ (z : X × Y), f z ∂μ.prod ν
      rw [prod_swap]All goals completed! 🐙

定理 (反復積分に対するフビニの定理).

f : X \times Y \to \mathbb{R} が \mu \times \nu に関して可積分であるとする。 \mu と \nu は S-有限であると仮定する。このとき \int_{x \in X} \int_{y \in Y} f(x,y)\,d\nu\,d\mu = \int_{y \in Y} \int_{x \in X} f(x,y)\,d\mu\,d\nu. が成り立つ。

Lean code

theorem integral_prod_swap' [SFinite μ] [SFinite ν] {f : X × Y → ℝ}
    (hf : Integrable f (μ.prod ν)) :
    ∫ x, ∫ y, f (x, y) ∂ν ∂μ = ∫ y, ∫ x, f (x, y) ∂μ ∂ν := byX:Type u_1Y:Type u_2inst✝³:MeasurableSpace Xinst✝²:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝¹:SFinite μinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (x : X), ∫ (y : Y), f (x, y) ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f (x, y) ∂μ ∂ν
  calc
    ∫ x, ∫ y, f (x, y) ∂ν ∂μ = ∫ z, f z ∂(μ.prod ν) := byX:Type u_1Y:Type u_2inst✝³:MeasurableSpace Xinst✝²:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝¹:SFinite μinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (x : X), ∫ (y : Y), f (x, y) ∂ν ∂μ = ∫ (z : X × Y), f z ∂μ.prod ν
      apply (integral_prod hf).symmAll goals completed! 🐙
    _ = ∫ z, f z.swap ∂(ν.prod μ) := byX:Type u_1Y:Type u_2inst✝³:MeasurableSpace Xinst✝²:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝¹:SFinite μinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (z : X × Y), f z ∂μ.prod ν = ∫ (z : Y × X), f z.swap ∂ν.prod μ
      apply (integral_prod_swap f hf.measurable).symmAll goals completed! 🐙
    _ = ∫ y, ∫ x, f (y, x).swap ∂μ ∂ν := byX:Type u_1Y:Type u_2inst✝³:MeasurableSpace Xinst✝²:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝¹:SFinite μinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (z : Y × X), f z.swap ∂ν.prod μ = ∫ (y : Y), ∫ (x : X), f (y, x).swap ∂μ ∂ν
      apply integral_prod hf.swapAll goals completed! 🐙
    _ = ∫ y, ∫ x, f (x, y) ∂μ ∂ν := byX:Type u_1Y:Type u_2inst✝³:MeasurableSpace Xinst✝²:MeasurableSpace Yμ:Measure Xν:Measure Yinst✝¹:SFinite μinst✝:SFinite νf:X × Y → ℝhf:Integrable f (μ.prod ν)⊢ ∫ (y : Y), ∫ (x : X), f (y, x).swap ∂μ ∂ν = ∫ (y : Y), ∫ (x : X), f (x, y) ∂μ ∂ν
      simp only [Prod.swap_prod_mk]All goals completed! 🐙