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 𝓧 𝓨
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_1 :
  (∀ᵐ (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_1 : ∀ᵐ (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_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
⊢ f (⨍ (x : 𝓨), ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, x)).toReal ∂(η : (a : 𝓧) → Measure 𝓨) a) ≤
    ⨍ (x : 𝓨), f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, x)).toReal ∂(η : (a : 𝓧) → Measure 𝓨) a

Tactic:
exact ConvexOn.map_average_le hf_cvx hf_cont isClosed_Ici (by simp) h_int' h_int

Premises used: ConvexOn.map_average_le, isClosed_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
hf_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
hf_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
hf_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
hf_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
hf_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
hf_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
hf_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
hf_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
hf_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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
⊢ ∃ (c : ℝ) (c' : ℝ), ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x

Tactic:
hf_cvx.exists_affine_le_real isClosed_Ici hf_cont.lowerSemicontinuousOn

Premises used: Set.Mem, ConvexOn.exists_affine_le_real, ContinuousOn.lowerSemicontinuousOn, isClosed_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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
obtain :
  ∀ (c c' : ℝ) (h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x), Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν

Tactic:
obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x :=
    hf_cvx.exists_affine_le_real isClosed_Ici hf_cont.lowerSemicontinuousOn

Premises used: ConvexOn.exists_affine_le_real, ContinuousOn.lowerSemicontinuousOn, isClosed_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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
funProp : ‖c'‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') ν

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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν
refine_2 :
  (ae ν).EventuallyLE (β := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal
refine_3 :
  (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (x : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal
refine_4 :
  Integrable (ε := ℝ)
    (fun (x : 𝓧) ↦
      @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal)
    ν
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) ν

Tactic:
refine integrable_of_le_of_le (f := fun a ↦ f (μ.rnDeriv ν a).toReal)
    (g₁ := fun x ↦ c * (μ.rnDeriv ν x).toReal + c')
    (g₂ := fun x ↦ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal ∂(η x))
    ?_ ?_ ?_ (by fun_prop) ?_

Premises used: MeasureTheory.integrable_of_le_of_le
-- 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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ StronglyMeasurable (β := ℝ) fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal

Tactic:
ae_of_all _ fun x ↦ h _ ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.rnDeriv, ENNReal.toReal_nonneg, ENNReal.toReal, MeasureTheory.ae_of_all, Filter.EventuallyLE
-- 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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (x : 𝓧) ↦ c * (μ.rnDeriv ν x).toReal + c') fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal

Tactic:
exact ae_of_all _ fun x ↦ h _ ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ENNReal.toReal, MeasureTheory.ae_of_all
-- 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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (x : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal

Tactic:
hf_cvx.apply_rnDeriv_ae_le_integral hf hf_cont_at hf_int hκη

Premises used: ConvexOn.apply_rnDeriv_ae_le_integral
-- 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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ (ae ν).EventuallyLE (β := ℝ) (fun (a : 𝓧) ↦ f (μ.rnDeriv ν a).toReal) fun (x : 𝓧) ↦
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal

Tactic:
exact hf_cvx.apply_rnDeriv_ae_le_integral hf hf_cont_at hf_int hκη

Premises used: ConvexOn.apply_rnDeriv_ae_le_integral
-- 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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (ε := ℝ)
    (fun (x : 𝓧) ↦
      @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal)
    ν

Tactic:
hf_int.integral_compProd

Premises used: MeasureTheory.Integrable.integral_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
hf_int : Integrable (ε := ℝ) (fun (p : 𝓧 × 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
c c' : ℝ
h : ∀ (x : ℝ), 0 ≤ x → c * x + c' ≤ f x
⊢ Integrable (ε := ℝ)
    (fun (x : 𝓧) ↦
      @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, b)).toReal)
    ν

Tactic:
exact hf_int.integral_compProd

Premises used: MeasureTheory.Integrable.integral_compProd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
rw :
  Measurable.{u_1, 0} (α := α)
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2 ∧
    (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
            ⋯).1 ⟂ₘ
        ν ∧
      μ =
        (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
              Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).1 +
          ν.withDensity
            (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
                Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2
⊢ Measurable (μ.rnDeriv ν) ∧ μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [singularPart, rnDeriv, dif_pos h, dif_pos h]

Premises used: MeasureTheory.Measure.rnDeriv, dif_pos, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable.{u_1, 0} (α := α)
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2 ∧
    (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
            ⋯).1 ⟂ₘ
        ν ∧
      μ =
        (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
              Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).1 +
          ν.withDensity
            (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
                Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2

Tactic:
Classical.choose_spec h.lebesgue_decomposition

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition, Classical.choose_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable.{u_1, 0} (α := α)
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2 ∧
    (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦ Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2)
            ⋯).1 ⟂ₘ
        ν ∧
      μ =
        (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
              Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).1 +
          ν.withDensity
            (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
                Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2

Tactic:
exact Classical.choose_spec h.lebesgue_decomposition

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition, Classical.choose_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
rw :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞)
    (if h : μ.HaveLebesgueDecomposition ν then
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).2
    else 0)
    0
rw₁ rw₂ : Eq.{u_1 + 1} (α := α → ℝ≥0∞) 0 0
⊢ μ.rnDeriv ν = 0

Tactic:
rw [rnDeriv, dif_neg h]

Premises used: MeasureTheory.Measure.rnDeriv, dif_neg
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
rw :
  Eq.{u_1 + 1} (α := Measure α)
    (if h : μ.HaveLebesgueDecomposition ν then
      (Classical.choose (p := fun (x : Measure α × (α → ℝ≥0∞)) ↦
          Measurable x.2 ∧ x.1 ⟂ₘ ν ∧ μ = x.1 + ν.withDensity x.2) ⋯).1
    else 0)
    0
rw₁ rw₂ : Eq.{u_1 + 1} (α := Measure α) 0 0
⊢ μ.singularPart ν = 0

Tactic:
rw [singularPart, dif_neg h]

Premises used: dif_neg, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (h : μ.HaveLebesgueDecomposition ν), Measurable (μ.rnDeriv ν)
neg : ∀ (h : ¬μ.HaveLebesgueDecomposition ν), Measurable (μ.rnDeriv ν)
⊢ Measurable (μ.rnDeriv ν)

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition