Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) →
            Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    IndepFun f g
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ IndepFun f g ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) → Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
refine' ⟨fun hfg _ _ hφ hψ => IndepFun.integral_mul_of_integrable (hfg.comp hφ hψ), _⟩
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) → Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) →
            Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    IndepFun f g
rintro h _ _ ⟨A, hA, rfl⟩ ⟨B, hB, rfl⟩
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (indicator A 1 ∘ f * indicator B 1 ∘ g) = integral μ (indicator A 1 ∘ f) * integral μ (indicator B 1 ∘ g)
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) → Integrable (ψ ∘ g) → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
specialize
  h (measurable_one.indicator hA) (measurable_one.indicator hB)
    ((integrable_const 1).indicator (hfm.comp measurable_id hA))
    ((integrable_const 1).indicator (hgm.comp measurable_id hB))
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (indicator A 1 ∘ f * indicator B 1 ∘ g) = integral μ (indicator A 1 ∘ f) * integral μ (indicator B 1 ∘ g)
⊢ ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B) ≠ ⊤
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (indicator A 1 ∘ f * indicator B 1 ∘ g) = integral μ (indicator A 1 ∘ f) * integral μ (indicator B 1 ∘ g)
⊢ ↑↑μ (f ⁻¹' A ∩ g ⁻¹' B) = ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B)
rwa [← ENNReal.toReal_eq_toReal (measure_ne_top μ _), ENNReal.toReal_mul, ←
  integral_indicator_one ((hfm hA).inter (hgm hB)), ← integral_indicator_one (hfm hA), ←
  integral_indicator_one (hgm hB), Set.inter_indicator_one]
no goals
case intro.intro.intro.intro
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f✝ g✝ : Ω → ℝ≥0∞
X Y : Ω → ℝ
inst✝ : IsFiniteMeasure μ
β : Type u_2
β' : Type u_3
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h : integral μ (indicator A 1 ∘ f * indicator B 1 ∘ g) = integral μ (indicator A 1 ∘ f) * integral μ (indicator B 1 ∘ g)
⊢ ↑↑μ (f ⁻¹' A) * ↑↑μ (g ⁻¹' B) ≠ ⊤
exact ENNReal.mul_ne_top (measure_ne_top μ _) (measure_ne_top μ _)