awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν
have neg : (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal
Tactic: refine (integrable_congr ?_).mpr hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal
have h : ∀ (x : 𝓧) (hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x), f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal
Tactic: filter_upwards [h_rnDeriv_eq] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
x : 𝓧
hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x
⊢ f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal
have h : f (μ.rnDeriv ν x).toReal = f (μ.rnDeriv ν x).toReal
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν'
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have neg : ∀ (h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν),
  ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
Tactic: rw [h_eq, mul_comm, ← div_le_iff₀, div_eq_inv_mul, inv_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν'
neg :
  ∀ (h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν),
    ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have neg₁ : ∀ (h : f (μ'.real univ) ≤ (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν) * (ν.real univ)⁻¹), 0 < (ν.real univ)⁻¹
Tactic: rw [h_eq, mul_comm, ← div_le_iff₀, div_eq_inv_mul, inv_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this_1 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have h₁ : μ.real univ / ν.real univ = μ'.real univ
Tactic: convert! h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsSFiniteKernel κ
inst_2 : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∀ᵐ (a : 𝓧) ∂μ,
    ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a =
      (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ
have 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 ∂μ
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (by fun_prop) (κ.measurable_coe .univ) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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 : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
have rw : ∫⁻ (x : 𝓧 × 𝓨) in SProd.sprod (β := Set 𝓨) s univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x ∂μ ⊗ₘ η =
  ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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 ∂μ
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
have rw₁ : (μ ⊗ₘ κ : (a : Set (𝓧 × 𝓨)) → ℝ≥0∞) (SProd.sprod (β := Set 𝓨) s univ) =
  ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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 ∂μ
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
    ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
have rw₂ : ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ =
  ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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∞)
⊢ ∫⁻ (x : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (x, b) ∂(η : (a : 𝓧) → Measure 𝓨) x ∂μ =
    ∫⁻ (x : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
have calc : ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
  ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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 ∂μ
⊢ ∫⁻ (x : 𝓧) in s, ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (x, b) ∂(η : (a : 𝓧) → Measure 𝓨) x ∂μ =
    ∫⁻ (x : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) x : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) univ ∂μ
have calc₁ : ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a ∂μ =
  ∫⁻ (a : 𝓧) in s, (((κ : (a : 𝓧) → Measure 𝓨) a : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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
⊢ ContinuousWithinAt f (Ici 0) x
have inl : ∀ (hx : Membership.mem (γ := Set ℝ) (Ici 0) 0), ContinuousWithinAt f (Ici 0) 0
Tactic: rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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
⊢ ContinuousWithinAt f (Ici 0) x
have inr : ∀ (hx_pos : 0 < x), ContinuousWithinAt f (Ici 0) x
Tactic: rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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 (Ici 0) x
have h : ContinuousWithinAt f (interior (Ici 0)) x
Tactic: have h := hf_cvx.continuousOn_interior x (by simpa)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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
⊢ ContinuousWithinAt f (Ici 0) x
have h₁ : ContinuousAt f x
Tactic: simp only [nonempty_Iio, interior_Ici',
        continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (a : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
have hf_cont : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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)
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (a : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
have h_lt_top : ∀ᵐ (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 (ν ⊗ₘ η)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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) < ∞
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (a : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
have h_integrable : Integrable (ε := ℝ) (fun (x : 𝓧 × 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η)
Tactic: have h_integrable : Integrable (fun x ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x).toReal) (ν ⊗ₘ η) :=
    Measure.integrable_toReal_rnDeriv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
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) (ν ⊗ₘ η)
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (a : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
have 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
Tactic: rw [Measure.integrable_compProd_iff] at h_integrable h_int
Cleared hypotheses: h_int, hκη, hf_cont, h_lt_top, h_integrable