[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
⊢ HasFiniteIntegral fun b => ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))
[PROOFSTEP]
let t := toMeasurable ((κ ⊗ₖ η) a) s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable (↑(κ ⊗ₖ η) a) s
⊢ HasFiniteIntegral fun b => ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))
[PROOFSTEP]
simp_rw [HasFiniteIntegral, ennnorm_eq_ofReal toReal_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable (↑(κ ⊗ₖ η) a) s
⊢ ∫⁻ (a_1 : β), ENNReal.ofReal (ENNReal.toReal (↑↑(↑η (a, a_1)) (Prod.mk a_1 ⁻¹' s))) ∂↑κ a < ⊤
[PROOFSTEP]
calc
  ∫⁻ b, ENNReal.ofReal (η (a, b) (Prod.mk b ⁻¹' s)).toReal ∂κ a
  _ ≤ ∫⁻ b, η (a, b) (Prod.mk b ⁻¹' t) ∂κ a := by
    refine' lintegral_mono_ae _
    filter_upwards [ae_kernel_lt_top a h2s] with b hb
    rw [ofReal_toReal hb.ne]
    exact measure_mono (preimage_mono (subset_toMeasurable _ _))
  _ ≤ (κ ⊗ₖ η) a t := (le_compProd_apply _ _ _ _)
  _ = (κ ⊗ₖ η) a s := (measure_toMeasurable s)
  _ < ⊤ := h2s.lt_top
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable (↑(κ ⊗ₖ η) a) s
⊢ ∫⁻ (b : β), ENNReal.ofReal (ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))) ∂↑κ a ≤
    ∫⁻ (b : β), ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' t) ∂↑κ a
[PROOFSTEP]
refine' lintegral_mono_ae _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable (↑(κ ⊗ₖ η) a) s
⊢ ∀ᵐ (a_1 : β) ∂↑κ a,
    ENNReal.ofReal (ENNReal.toReal (↑↑(↑η (a, a_1)) (Prod.mk a_1 ⁻¹' s))) ≤ ↑↑(↑η (a, a_1)) (Prod.mk a_1 ⁻¹' t)
[PROOFSTEP]
filter_upwards [ae_kernel_lt_top a h2s] with b hb
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable (↑(κ ⊗ₖ η) a) s
b : β
hb : ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
⊢ ENNReal.ofReal (ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))) ≤
    ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' toMeasurable (↑(κ ⊗ₖ η) a) s)
[PROOFSTEP]
rw [ofReal_toReal hb.ne]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable (↑(κ ⊗ₖ η) a) s
b : β
hb : ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
⊢ ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s) ≤ ↑↑(↑η (a, b)) (Prod.mk b ⁻¹' toMeasurable (↑(κ ⊗ₖ η) a) s)
[PROOFSTEP]
exact measure_mono (preimage_mono (subset_toMeasurable _ _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
⊢ Integrable fun b => ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
⊢ AEStronglyMeasurable (fun b => ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))) (↑κ a)
[PROOFSTEP]
exact (measurable_kernel_prod_mk_left' hs a).ennreal_toReal.aestronglyMeasurable
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a✝ a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s ≠ ⊤
⊢ HasFiniteIntegral fun b => ENNReal.toReal (↑↑(↑η (a, b)) (Prod.mk b ⁻¹' s))
[PROOFSTEP]
exact hasFiniteIntegral_prod_mk_left a h2s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁴ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝³ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝² : IsSFiniteKernel η
a : α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : β × γ → E
hf : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ (fun x => ∫ (y : γ), f (x, y) ∂↑η (a, x)) =ᵐ[↑κ a] fun x => ∫ (y : γ), AEStronglyMeasurable.mk f hf (x, y) ∂↑η (a, x)
[PROOFSTEP]
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝² : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝¹ : IsSFiniteKernel η
a : α
δ : Type u_5
inst✝ : TopologicalSpace δ
f : β × γ → δ
hf : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ ∀ᵐ (x : β) ∂↑κ a, AEStronglyMeasurable (fun y => f (x, y)) (↑η (a, x))
[PROOFSTEP]
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with x hx using
  ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prod_mk_left, hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
⊢ HasFiniteIntegral f ↔
    (∀ᵐ (x : β) ∂↑κ a, HasFiniteIntegral fun y => f (x, y)) ∧
      HasFiniteIntegral fun x => ∫ (y : γ), ‖f (x, y)‖ ∂↑η (a, x)
[PROOFSTEP]
simp only [HasFiniteIntegral]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
⊢ ∫⁻ (a : β × γ), ↑‖f a‖₊ ∂↑(κ ⊗ₖ η) a < ⊤ ↔
    (∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤) ∧
      ∫⁻ (a_1 : β), ↑‖∫ (y : γ), ‖f (a_1, y)‖ ∂↑η (a, a_1)‖₊ ∂↑κ a < ⊤
[PROOFSTEP]
rw [kernel.lintegral_compProd _ _ _ h1f.ennnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ ↔
    (∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤) ∧
      ∫⁻ (a_1 : β), ↑‖∫ (y : γ), ‖f (a_1, y)‖ ∂↑η (a, a_1)‖₊ ∂↑κ a < ⊤
[PROOFSTEP]
have : ∀ x, ∀ᵐ y ∂η (a, x), 0 ≤ ‖f (x, y)‖ := fun x => eventually_of_forall fun y => norm_nonneg _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ ↔
    (∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤) ∧
      ∫⁻ (a_1 : β), ↑‖∫ (y : γ), ‖f (a_1, y)‖ ∂↑η (a, a_1)‖₊ ∂↑κ a < ⊤
[PROOFSTEP]
simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
    (h1f.norm.comp_measurable measurable_prod_mk_left).aestronglyMeasurable,
  ennnorm_eq_ofReal toReal_nonneg, ofReal_norm_eq_coe_nnnorm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ ↔
    (∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤) ∧
      ∫⁻ (a_1 : β), ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂↑η (a, a_1))) ∂↑κ a < ⊤
[PROOFSTEP]
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
  rw [← and_congr_right_iff, and_iff_right_of_imp h1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)
[PROOFSTEP]
rw [← and_congr_right_iff, and_iff_right_of_imp h1]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ ↔
    (∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤) ∧
      ∫⁻ (a_1 : β), ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂↑η (a, a_1))) ∂↑κ a < ⊤
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ (∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤) →
    (∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ ↔
      ∫⁻ (a_2 : β), ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_2, a)‖₊ ∂↑η (a, a_2))) ∂↑κ a < ⊤)
[PROOFSTEP]
intro h2f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ ↔
    ∫⁻ (a_1 : β), ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂↑η (a, a_1))) ∂↑κ a < ⊤
[PROOFSTEP]
rw [lintegral_congr_ae]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ (fun b => ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b)) =ᵐ[↑κ a] fun a_1 =>
    ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂↑η (a, a_1)))
[PROOFSTEP]
refine' h2f.mp _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ ∀ᵐ (x : β) ∂↑κ a,
    ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤ →
      (fun b => ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b)) x =
        (fun a_2 => ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_2, a)‖₊ ∂↑η (a, a_2)))) x
[PROOFSTEP]
apply eventually_of_forall
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ ∀ (x : β),
    ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤ →
      (fun b => ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b)) x =
        (fun a_2 => ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_2, a)‖₊ ∂↑η (a, a_2)))) x
[PROOFSTEP]
intro x hx
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
x : β
hx : ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ (fun b => ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b)) x =
    (fun a_1 => ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (a_1, a)‖₊ ∂↑η (a, a_1)))) x
[PROOFSTEP]
dsimp only
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
x : β
hx : ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ ∫⁻ (c : γ), ↑‖f (x, c)‖₊ ∂↑η (a, x) = ENNReal.ofReal (ENNReal.toReal (∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x)))
[PROOFSTEP]
rw [ofReal_toReal]
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
x : β
hx : ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) ≠ ⊤
[PROOFSTEP]
rw [← lt_top_iff_ne_top]
[GOAL]
case hp
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
x : β
hx : ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
⊢ ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤ → ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
[PROOFSTEP]
intro h2f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤
⊢ ∀ᵐ (x : β) ∂↑κ a, ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x) < ⊤
[PROOFSTEP]
refine' ae_lt_top _ h2f.ne
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : StronglyMeasurable f
this✝ : ∀ (x : β), ∀ᵐ (y : γ) ∂↑η (a, x), 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (b : β), ∫⁻ (c : γ), ↑‖f (b, c)‖₊ ∂↑η (a, b) ∂↑κ a < ⊤
⊢ Measurable fun x => ∫⁻ (a : γ), ↑‖f (x, a)‖₊ ∂↑η (a, x)
[PROOFSTEP]
exact h1f.ennnorm.lintegral_kernel_prod_right''
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ HasFiniteIntegral f ↔
    (∀ᵐ (x : β) ∂↑κ a, HasFiniteIntegral fun y => f (x, y)) ∧
      HasFiniteIntegral fun x => ∫ (y : γ), ‖f (x, y)‖ ∂↑η (a, x)
[PROOFSTEP]
rw [hasFiniteIntegral_congr h1f.ae_eq_mk, hasFiniteIntegral_compProd_iff h1f.stronglyMeasurable_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ ((∀ᵐ (x : β) ∂↑κ a, HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ∧
      HasFiniteIntegral fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂↑η (a, x)) ↔
    (∀ᵐ (x : β) ∂↑κ a, HasFiniteIntegral fun y => f (x, y)) ∧
      HasFiniteIntegral fun x => ∫ (y : γ), ‖f (x, y)‖ ∂↑η (a, x)
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ (∀ᵐ (x : β) ∂↑κ a, HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔
    ∀ᵐ (x : β) ∂↑κ a, HasFiniteIntegral fun y => f (x, y)
[PROOFSTEP]
apply eventually_congr
[GOAL]
case h₁.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ ∀ᵐ (x : β) ∂↑κ a,
    (HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔ HasFiniteIntegral fun y => f (x, y)
[PROOFSTEP]
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ ∀ (a_1 : β),
    (∀ᵐ (c : γ) ∂↑η (a, a_1), AEStronglyMeasurable.mk f h1f (a_1, c) = f (a_1, c)) →
      ((HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (a_1, y)) ↔ HasFiniteIntegral fun y => f (a_1, y))
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
x : β
hx : ∀ᵐ (c : γ) ∂↑η (a, x), AEStronglyMeasurable.mk f h1f (x, c) = f (x, c)
⊢ (HasFiniteIntegral fun y => AEStronglyMeasurable.mk f h1f (x, y)) ↔ HasFiniteIntegral fun y => f (x, y)
[PROOFSTEP]
exact hasFiniteIntegral_congr hx
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ (HasFiniteIntegral fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂↑η (a, x)) ↔
    HasFiniteIntegral fun x => ∫ (y : γ), ‖f (x, y)‖ ∂↑η (a, x)
[PROOFSTEP]
apply hasFiniteIntegral_congr
[GOAL]
case h₂.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
h1f : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂↑η (a, x)) =ᵐ[↑κ a] fun x =>
    ∫ (y : γ), ‖f (x, y)‖ ∂↑η (a, x)
[PROOFSTEP]
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with _ hx using integral_congr_ae (EventuallyEq.fun_comp hx _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝¹ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → E
hf : AEStronglyMeasurable f (↑(κ ⊗ₖ η) a)
⊢ Integrable f ↔ (∀ᵐ (x : β) ∂↑κ a, Integrable fun y => f (x, y)) ∧ Integrable fun x => ∫ (y : γ), ‖f (x, y)‖ ∂↑η (a, x)
[PROOFSTEP]
simp only [Integrable, hasFiniteIntegral_compProd_iff' hf, hf.norm.integral_kernel_compProd, hf, hf.compProd_mk_left,
  eventually_and, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ ∫ (x : β), F (∫ (y : γ), f (x, y) + g (x, y) ∂↑η (a, x)) ∂↑κ a =
    ∫ (x : β), F (∫ (y : γ), f (x, y) ∂↑η (a, x) + ∫ (y : γ), g (x, y) ∂↑η (a, x)) ∂↑κ a
[PROOFSTEP]
refine' integral_congr_ae _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ (fun x => F (∫ (y : γ), f (x, y) + g (x, y) ∂↑η (a, x))) =ᵐ[↑κ a] fun x =>
    F (∫ (y : γ), f (x, y) ∂↑η (a, x) + ∫ (y : γ), g (x, y) ∂↑η (a, x))
[PROOFSTEP]
filter_upwards [hf.compProd_mk_left_ae, hg.compProd_mk_left_ae] with _ h2f h2g
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f
hg : Integrable g
a✝ : β
h2f : Integrable fun y => f (a✝, y)
h2g : Integrable fun y => g (a✝, y)
⊢ F (∫ (y : γ), f (a✝, y) + g (a✝, y) ∂↑η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂↑η (a, a✝) + ∫ (y : γ), g (a✝, y) ∂↑η (a, a✝))
[PROOFSTEP]
simp [integral_add h2f h2g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ ∫ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂↑η (a, x)) ∂↑κ a =
    ∫ (x : β), F (∫ (y : γ), f (x, y) ∂↑η (a, x) - ∫ (y : γ), g (x, y) ∂↑η (a, x)) ∂↑κ a
[PROOFSTEP]
refine' integral_congr_ae _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ (fun x => F (∫ (y : γ), f (x, y) - g (x, y) ∂↑η (a, x))) =ᵐ[↑κ a] fun x =>
    F (∫ (y : γ), f (x, y) ∂↑η (a, x) - ∫ (y : γ), g (x, y) ∂↑η (a, x))
[PROOFSTEP]
filter_upwards [hf.compProd_mk_left_ae, hg.compProd_mk_left_ae] with _ h2f h2g
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f
hg : Integrable g
a✝ : β
h2f : Integrable fun y => f (a✝, y)
h2g : Integrable fun y => g (a✝, y)
⊢ F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂↑η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂↑η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂↑η (a, a✝))
[PROOFSTEP]
simp [integral_sub h2f h2g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → ℝ≥0∞
hf : Integrable f
hg : Integrable g
⊢ ∫⁻ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂↑η (a, x)) ∂↑κ a =
    ∫⁻ (x : β), F (∫ (y : γ), f (x, y) ∂↑η (a, x) - ∫ (y : γ), g (x, y) ∂↑η (a, x)) ∂↑κ a
[PROOFSTEP]
refine' lintegral_congr_ae _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → ℝ≥0∞
hf : Integrable f
hg : Integrable g
⊢ (fun x => F (∫ (y : γ), f (x, y) - g (x, y) ∂↑η (a, x))) =ᵐ[↑κ a] fun x =>
    F (∫ (y : γ), f (x, y) ∂↑η (a, x) - ∫ (y : γ), g (x, y) ∂↑η (a, x))
[PROOFSTEP]
filter_upwards [hf.compProd_mk_left_ae, hg.compProd_mk_left_ae] with _ h2f h2g
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → ℝ≥0∞
hf : Integrable f
hg : Integrable g
a✝ : β
h2f : Integrable fun y => f (a✝, y)
h2g : Integrable fun y => g (a✝, y)
⊢ F (∫ (y : γ), f (a✝, y) - g (a✝, y) ∂↑η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂↑η (a, a✝) - ∫ (y : γ), g (a✝, y) ∂↑η (a, a✝))
[PROOFSTEP]
simp [integral_sub h2f h2g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ Continuous fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ (x : { x // x ∈ Lp E 1 }), ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂↑η (a, x) ∂↑κ a) x
[PROOFSTEP]
intro g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂↑η (a, x) ∂↑κ a) g
[PROOFSTEP]
refine'
  tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd
    (eventually_of_forall fun h => (L1.integrable_coeFn h).integral_compProd) _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ Tendsto (fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) ∂↑η (a, x) - ∫ (y : γ), ↑↑g (x, y) ∂↑η (a, x)‖₊ ∂↑κ a) (𝓝 g)
    (𝓝 0)
[PROOFSTEP]
simp_rw [← kernel.lintegral_fn_integral_sub (fun x => (‖x‖₊ : ℝ≥0∞)) (L1.integrable_coeFn _) (L1.integrable_coeFn g)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ Tendsto (fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂↑η (a, x)‖₊ ∂↑κ a) (𝓝 g) (𝓝 0)
[PROOFSTEP]
refine' tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le _) _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ { x // x ∈ Lp E 1 } → ℝ≥0∞
[PROOFSTEP]
exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖₊ ∂η (a, x) ∂κ a
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂↑η (a, x) ∂↑κ a) (𝓝 g) (𝓝 0)
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ (fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂↑η (a, x)‖₊ ∂↑κ a) ≤ fun i =>
    ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
swap
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ (fun i => ∫⁻ (x : β), ↑‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂↑η (a, x)‖₊ ∂↑κ a) ≤ fun i =>
    ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
exact fun i => lintegral_mono fun x => ennnorm_integral_le_lintegral_ennnorm _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂↑η (a, x) ∂↑κ a) (𝓝 g) (𝓝 0)
[PROOFSTEP]
show Tendsto (fun i : β × γ →₁[(κ ⊗ₖ η) a] E => ∫⁻ x, ∫⁻ y : γ, ‖i (x, y) - g (x, y)‖₊ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂↑η (a, x) ∂↑κ a) (𝓝 g) (𝓝 0)
[PROOFSTEP]
have :
  ∀ i : (MeasureTheory.Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))),
    Measurable fun z => (‖i z - g z‖₊ : ℝ≥0∞) :=
  fun i => ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).ennnorm
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
this : ∀ (i : { x // x ∈ Lp E 1 }), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂↑η (a, x) ∂↑κ a) (𝓝 g) (𝓝 0)
[PROOFSTEP]
simp_rw [← kernel.lintegral_compProd _ _ _ (this _), ← L1.ofReal_norm_sub_eq_lintegral, ← ofReal_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
this : ∀ (i : { x // x ∈ Lp E 1 }), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊
⊢ Tendsto (fun i => ENNReal.ofReal ‖i - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
[PROOFSTEP]
refine' (continuous_ofReal.tendsto 0).comp _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
this : ∀ (i : { x // x ∈ Lp E 1 }), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊
⊢ Tendsto (fun i => ‖i - g‖) (𝓝 g) (𝓝 0)
[PROOFSTEP]
rw [← tendsto_iff_norm_tendsto_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
g : { x // x ∈ Lp E 1 }
this : ∀ (i : { x // x ∈ Lp E 1 }), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊
⊢ Tendsto (fun i => i) (𝓝 g) (𝓝 g)
[PROOFSTEP]
exact tendsto_id
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ {f : β × γ → E}, Integrable f → ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
apply Integrable.induction
[GOAL]
case h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ (c : E) ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ↑↑(↑(κ ⊗ₖ η) a) s < ⊤ →
        ∫ (z : β × γ), indicator s (fun x => c) z ∂↑(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), indicator s (fun x => c) (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
intro c s hs h2s
[GOAL]
case h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ∫ (z : β × γ), indicator s (fun x => c) z ∂↑(κ ⊗ₖ η) a =
    ∫ (x : β), ∫ (y : γ), indicator s (fun x => c) (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp, integral_indicator (measurable_prod_mk_left hs),
  MeasureTheory.set_integral_const, integral_smul_const]
[GOAL]
case h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ENNReal.toReal (↑↑(↑(κ ⊗ₖ η) a) s) • c = (∫ (x : β), ENNReal.toReal (↑↑(↑η (a, x)) (Prod.mk x ⁻¹' s)) ∂↑κ a) • c
[PROOFSTEP]
congr 1
[GOAL]
case h_ind.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ENNReal.toReal (↑↑(↑(κ ⊗ₖ η) a) s) = ∫ (x : β), ENNReal.toReal (↑↑(↑η (a, x)) (Prod.mk x ⁻¹' s)) ∂↑κ a
[PROOFSTEP]
rw [integral_toReal]
[GOAL]
case h_ind.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ENNReal.toReal (↑↑(↑(κ ⊗ₖ η) a) s) = ENNReal.toReal (∫⁻ (a_1 : β), ↑↑(↑η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂↑κ a)
case h_ind.e_a.hfm
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ AEMeasurable fun x => ↑↑(↑η (a, x)) (Prod.mk x ⁻¹' s)
case h_ind.e_a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ∀ᵐ (x : β) ∂↑κ a, ↑↑(↑η (a, x)) (Prod.mk x ⁻¹' s) < ⊤
[PROOFSTEP]
rotate_left
[GOAL]
case h_ind.e_a.hfm
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ AEMeasurable fun x => ↑↑(↑η (a, x)) (Prod.mk x ⁻¹' s)
[PROOFSTEP]
exact (kernel.measurable_kernel_prod_mk_left' hs _).aemeasurable
[GOAL]
case h_ind.e_a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ∀ᵐ (x : β) ∂↑κ a, ↑↑(↑η (a, x)) (Prod.mk x ⁻¹' s) < ⊤
[PROOFSTEP]
exact ae_kernel_lt_top a h2s.ne
[GOAL]
case h_ind.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ENNReal.toReal (↑↑(↑(κ ⊗ₖ η) a) s) = ENNReal.toReal (∫⁻ (a_1 : β), ↑↑(↑η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂↑κ a)
[PROOFSTEP]
rw [kernel.compProd_apply _ _ _ hs]
[GOAL]
case h_ind.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ↑↑(↑(κ ⊗ₖ η) a) s < ⊤
⊢ ENNReal.toReal (∫⁻ (b : β), ↑↑(↑η (a, b)) {c | (b, c) ∈ s} ∂↑κ a) =
    ENNReal.toReal (∫⁻ (a_1 : β), ↑↑(↑η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂↑κ a)
[PROOFSTEP]
rfl
[GOAL]
case h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ ⦃f g : β × γ → E⦄,
    Disjoint (support f) (support g) →
      Integrable f →
        Integrable g →
          ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a →
            ∫ (z : β × γ), g z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂↑η (a, x) ∂↑κ a →
              ∫ (z : β × γ), (f + g) z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
intro f g _ i_f i_g hf hg
[GOAL]
case h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
a✝ : Disjoint (support f) (support g)
i_f : Integrable f
i_g : Integrable g
hf : ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
hg : ∫ (z : β × γ), g z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂↑η (a, x) ∂↑κ a
⊢ ∫ (z : β × γ), (f + g) z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
simp_rw [integral_add' i_f i_g, kernel.integral_integral_add' i_f i_g, hf, hg]
[GOAL]
case h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ IsClosed {f | ∫ (z : β × γ), ↑↑f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂↑η (a, x) ∂↑κ a}
[PROOFSTEP]
exact isClosed_eq continuous_integral kernel.continuous_integral_integral
[GOAL]
case h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ ⦃f g : β × γ → E⦄,
    f =ᵐ[↑(κ ⊗ₖ η) a] g →
      Integrable f →
        ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a →
          ∫ (z : β × γ), g z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
intro f g hfg _ hf
[GOAL]
case h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
hfg : f =ᵐ[↑(κ ⊗ₖ η) a] g
a✝ : Integrable f
hf : ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
⊢ ∫ (z : β × γ), g z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
convert hf using 1
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
hfg : f =ᵐ[↑(κ ⊗ₖ η) a] g
a✝ : Integrable f
hf : ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
⊢ ∫ (z : β × γ), g z ∂↑(κ ⊗ₖ η) a = ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a
[PROOFSTEP]
exact integral_congr_ae hfg.symm
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
hfg : f =ᵐ[↑(κ ⊗ₖ η) a] g
a✝ : Integrable f
hf : ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
⊢ ∫ (x : β), ∫ (y : γ), g (x, y) ∂↑η (a, x) ∂↑κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
refine' integral_congr_ae _
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
hfg : f =ᵐ[↑(κ ⊗ₖ η) a] g
a✝ : Integrable f
hf : ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
⊢ (fun x => ∫ (y : γ), g (x, y) ∂↑η (a, x)) =ᵐ[↑κ a] fun x => ∫ (y : γ), f (x, y) ∂↑η (a, x)
[PROOFSTEP]
refine' (ae_ae_of_ae_compProd hfg).mp (eventually_of_forall _)
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
hfg : f =ᵐ[↑(κ ⊗ₖ η) a] g
a✝ : Integrable f
hf : ∫ (z : β × γ), f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
⊢ ∀ (x : β),
    (∀ᵐ (c : γ) ∂↑η (a, x), f (x, c) = g (x, c)) →
      (fun x => ∫ (y : γ), g (x, y) ∂↑η (a, x)) x = (fun x => ∫ (y : γ), f (x, y) ∂↑η (a, x)) x
[PROOFSTEP]
exact fun x hfgx => integral_congr_ae (ae_eq_symm hfgx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t)
⊢ ∫ (z : β × γ) in s ×ˢ t, f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
rw [← kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht, integral_compProd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t)
⊢ ∫ (x : β), ∫ (y : γ), f (x, y) ∂↑(kernel.restrict η ht) (a, x) ∂↑(kernel.restrict κ hs) a =
    ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
simp_rw [kernel.restrict_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t)
⊢ Integrable fun z => f z
[PROOFSTEP]
rw [compProd_restrict, kernel.restrict_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : β × γ → E
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t)
⊢ Integrable fun z => f z
[PROOFSTEP]
exact hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : β × γ → E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ univ)
⊢ ∫ (z : β × γ) in s ×ˢ univ, f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
simp_rw [set_integral_compProd hs MeasurableSet.univ hf, Measure.restrict_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝⁷ : NormedAddCommGroup E
κ : { x // x ∈ kernel α β }
inst✝⁶ : IsSFiniteKernel κ
η : { x // x ∈ kernel (α × β) γ }
inst✝⁵ : IsSFiniteKernel η
a : α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f : β × γ → E
t : Set γ
ht : MeasurableSet t
hf : IntegrableOn f (univ ×ˢ t)
⊢ ∫ (z : β × γ) in univ ×ˢ t, f z ∂↑(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂↑η (a, x) ∂↑κ a
[PROOFSTEP]
simp_rw [set_integral_compProd MeasurableSet.univ ht hf, Measure.restrict_univ]