α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ((∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ∧
      HasFiniteIntegral fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => f (x, y)) ∧ HasFiniteIntegral fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ HasFiniteIntegral f ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => f (x, y)) ∧ HasFiniteIntegral fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
  hasFiniteIntegral_prod_iff h1f.stronglyMeasurable_mk]
case h₁
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔
    ∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => f (x, y)

case h₂
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (HasFiniteIntegral fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) ↔
    HasFiniteIntegral fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ((∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ∧
      HasFiniteIntegral fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => f (x, y)) ∧ HasFiniteIntegral fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
apply and_congr
case h₁.h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ∀ᵐ (x : α) ∂μ, (HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔ HasFiniteIntegral fun y => f (x, y)
case h₁
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔
    ∀ᵐ (x : α) ∂μ, HasFiniteIntegral fun y => f (x, y)
apply eventually_congr
case h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ∀ (a : α),
    (∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a, y) = f (a, y)) →
      ((HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (a, y)) ↔ HasFiniteIntegral fun y => f (a, y))
case h₁.h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ∀ᵐ (x : α) ∂μ, (HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔ HasFiniteIntegral fun y => f (x, y)
filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm]
case h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)
⊢ (HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔ HasFiniteIntegral fun y => f (x, y)
case h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ ∀ (a : α),
    (∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a, y) = f (a, y)) →
      ((HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (a, y)) ↔ HasFiniteIntegral fun y => f (a, y))
intro x hx
no goals
case h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)
⊢ (HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔ HasFiniteIntegral fun y => f (x, y)
exact hasFiniteIntegral_congr hx
case h₂.h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) =ᶠ[ae μ] fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
case h₂
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (HasFiniteIntegral fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) ↔
    HasFiniteIntegral fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
apply hasFiniteIntegral_congr
no goals
case h₂.h
α : Type u_1
α' : Type ?u.2393859
β : Type u_2
β' : Type ?u.2393865
γ : Type ?u.2393868
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ (fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) =ᶠ[ae μ] fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm] with _ hx using
  integral_congr_ae (EventuallyEq.fun_comp hx _)