-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integral_compProd :
    ∀ {f : β × γ → E} (_ : Integrable f ((κ ⊗ₖ η) a)),
      ∫ z, f z ∂(κ ⊗ₖ η) a = ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a

Proof state:
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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae ((κ ⊗ₖ η) a)] g
a✝ : Integrable f ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a

Tactic:
exact integral_congr_ae hfg.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
⊢ ∀ {f : β × γ → E},
    Integrable f ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : ¬CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : ¬CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

Tactic:
simp [integral, hE]

Result:
no goals

Proof state:
case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ (((κ ⊗ₖ η) a) s).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal

case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ AEMeasurable (fun x => (η (a, x)) (Prod.mk x ⁻¹' s)) (κ a)

case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ ∀ᵐ (x : β) ∂κ a, (η (a, x)) (Prod.mk x ⁻¹' s) < ⊤

Tactic:
rotate_left

Result:
case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ AEMeasurable (fun x => (η (a, x)) (Prod.mk x ⁻¹' s)) (κ a)

case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ ∀ᵐ (x : β) ∂κ a, (η (a, x)) (Prod.mk x ⁻¹' s) < ⊤

case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ (((κ ⊗ₖ η) a) s).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal

Proof state:
case pos.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
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ (∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal

Tactic:
rfl

Result:
no goals

Proof state:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ ∫ (z : β × γ), s.indicator (fun x => c) z ∂(κ ⊗ₖ η) a =
    ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) (x, y) ∂η (a, x) ∂κ a

Tactic:
simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
  integral_indicator (measurable_prod_mk_left hs), MeasureTheory.setIntegral_const,
  integral_smul_const]

Result:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ (((κ ⊗ₖ η) a) s).toReal • c = (∫ (x : β), ((η (a, x)) (Prod.mk x ⁻¹' s)).toReal ∂κ a) • c

Proof state:
case pos.h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : β × γ), ↑↑f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a}

Tactic:
exact isClosed_eq continuous_integral Kernel.continuous_integral_integral

Result:
no goals