-- Mathlib/Probability/Kernel/WithDensity.lean
theorem IsSFiniteKernel.withDensity (κ : Kernel α β) [IsSFiniteKernel κ]
    (hf_ne_top : ∀ a b, f a b ≠ ∞) : IsSFiniteKernel (withDensity κ f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
have h_eq_sum : withDensity κ f = Kernel.sum fun i => withDensity (seq κ i) f := by
  rw [← withDensity_kernel_sum _ _]
  congr
  exact (kernel_sum_seq κ).symm

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
h_eq_sum : κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f
⊢ IsSFiniteKernel (κ.withDensity f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
h_eq_sum : κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f
⊢ IsSFiniteKernel (Kernel.sum fun i => (κ.seq i).withDensity f)

Tactic:
exact isSFiniteKernel_sum (hκs := fun n =>
  isSFiniteKernel_withDensity_of_isFiniteKernel (seq κ n) hf_ne_top)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f

Tactic:
rw [← withDensity_kernel_sum _ _]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ κ.withDensity f = (Kernel.sum κ.seq).withDensity f

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
h_eq_sum : κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [h_eq_sum]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
h_eq_sum : κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f
⊢ IsSFiniteKernel (Kernel.sum fun i => (κ.seq i).withDensity f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ κ.withDensity f = (Kernel.sum κ.seq).withDensity f

Tactic:
congr

Result:
case e_κ
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ κ = Kernel.sum κ.seq

Proof state:
case e_κ
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤
⊢ κ = Kernel.sum κ.seq

Tactic:
exact (kernel_sum_seq κ).symm

Result:
no goals