awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Measurable (β := ℝ≥0∞) fun (a : 𝓧) ↦ ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
refine :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (x, b) ∂(η : (a : 𝓧) → Measure 𝓨) x ∂μ =
          ∫⁻ (x : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
⊢ ∀ᵐ (a : 𝓧) ∂μ,
    ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a =
      (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (κ.measurable_coe .univ) ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite, ProbabilityTheory.Kernel.measurable_coe, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  ∫⁻ (x : 𝓧 × 𝓨) in SProd.sprod (β := Set 𝓨) s univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x ∂μ ⊗ₘ η =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
rw₁ :
  (μ ⊗ₘ κ : (a : Set (𝓧 × 𝓨)) → ℝ≥0∞) (SProd.sprod (β := Set 𝓨) s univ) =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
rw₂ rw₃ :
  ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ

Tactic:
rw [← Measure.setLIntegral_compProd (by fun_prop) hs .univ, Measure.setLIntegral_rnDeriv hκη,
      Measure.compProd_apply_prod hs .univ]

Premises used: MeasureTheory.Measure.setLIntegral_rnDeriv, MeasureTheory.Measure.compProd_apply_prod, MeasureTheory.Measure.setLIntegral_compProd, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
calc :
  ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ
calc₁ :
  ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
⊢ ∫⁻ (x : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (x, b) ∂(η : (a : 𝓧) → Measure 𝓨) x ∂μ =
    ∫⁻ (x : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ

Tactic:
calc ∫⁻ a in s, ∫⁻ b, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η a) ∂μ
  _ = ∫⁻ a in s, ∫⁻ b in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η a) ∂μ := by simp
  _ = ∫⁻ a in s, (κ a) univ ∂μ := by
    rw [← Measure.setLIntegral_compProd (by fun_prop) hs .univ, Measure.setLIntegral_rnDeriv hκη,
      Measure.compProd_apply_prod hs .univ]

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
inl : ∀ (hx : Membership.mem (γ := Set ℝ) (Ici 0) 0), ContinuousWithinAt f (Ici 0) 0
inr : ∀ (hx_pos : 0 < x), ContinuousWithinAt f (Ici 0) x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hx : Membership.mem (γ := Set ℝ) (Ici 0) 0
⊢ ContinuousWithinAt f (Ici 0) 0

Tactic:
hf_cont_at
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hx : Membership.mem (γ := Set ℝ) (Ici 0) 0
⊢ ContinuousWithinAt f (Ici 0) 0

Tactic:
exact hf_cont_at
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
⊢ Membership.mem (γ := Set ℝ) (interior (Ici 0)) x

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
⊢ ContinuousWithinAt f (interior (Ici 0)) x

Tactic:
have h := hf_cvx.continuousOn_interior x (by simpa)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : ContinuousWithinAt f (interior (Ici 0)) x
⊢ ContinuousAt f x

Tactic:
simp only [nonempty_Iio, interior_Ici',
        continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h

Premises used: Ioi_mem_nhds, continuousWithinAt_iff_continuousAt, Set.nonempty_Iio, interior_Ici'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
h.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ici 0) x
hx_pos : 0 < x
h : ContinuousAt f x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
exact h.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ContinuousOn f (Ici 0)

Tactic:
have hf_cont : ContinuousOn f (Ici 0) := by
    intro x hx
    rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
    · exact hf_cont_at
    · have h := hf_cvx.continuousOn_interior x (by simpa)
      simp only [nonempty_Iio, interior_Ici',
        continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h
      exact h.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
⊢ ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞

Tactic:
have h_lt_top : ∀ᵐ a ∂ν, ∀ᵐ b ∂η a, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞ :=
    Measure.ae_ae_of_ae_compProd <| (μ ⊗ₘ κ).rnDeriv_lt_top (ν ⊗ₘ η)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
⊢ Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)

Tactic:
have h_integrable : Integrable (fun x ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η) :=
    Measure.integrable_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
rw :
  ∀
    (h_int :
      (∀ᵐ (x : 𝓧) ∂ν,
          @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
            ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
        Integrable (ε := ℝ)
          (fun (x : 𝓧) ↦
            @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦
              ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
          ν)
    (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) (hf_cont : ContinuousOn f (Ici 0))
    (h_lt_top :
      ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞)
    (h_integrable :
      (∀ᵐ (x : 𝓧) ∂ν,
          @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
            ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
        Integrable (ε := ℝ)
          (fun (x : 𝓧) ↦
            @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦
              ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
          ν),
    (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (a : 𝓧) ↦
      @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
rw₁ :
  ∀
    (h_integrable :
      (∀ᵐ (x : 𝓧) ∂ν,
          @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
            ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
        Integrable (ε := ℝ)
          (fun (x : 𝓧) ↦
            @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦
              ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
          ν),
    AEStronglyMeasurable (β := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
rw₂ : AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (a : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal

Tactic:
rw [Measure.integrable_compProd_iff] at h_integrable h_int

Premises used: MeasureTheory.Measure.integrable_compProd_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
⊢ StronglyMeasurable (β := ℝ) fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
⊢ AEStronglyMeasurable (β := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
⊢ StronglyMeasurable (β := ℝ) fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)

Tactic:
exact StronglyMeasurable.aestronglyMeasurable (by fun_prop)

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h :
  ∀ (a : 𝓧)
    (ha :
      μ.rnDeriv ν a ≠ 0 →
        ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a =
          (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ),
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
⊢ ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a

Tactic:
filter_upwards [Measure.ae_rnDeriv_ne_zero_imp_of_ae _ (lintegral_rnDeriv_compProd hκη)]
      with a ha

Premises used: MeasureTheory.Measure.ae_rnDeriv_ne_zero_imp_of_ae, MeasureTheory.lintegral_rnDeriv_compProd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
a : 𝓧
ha :
  μ.rnDeriv ν a ≠ 0 →
    ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a =
      (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ
pos :
  ∀ (h0 : μ.rnDeriv ν a = 0),
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
neg :
  ∀ (h0 : ¬μ.rnDeriv ν a = 0),
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
⊢ μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a

Tactic:
by_cases h0 : μ.rnDeriv ν a = 0

Premises used: MeasureTheory.Measure.rnDeriv