awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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 : NeZero ν
μ' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
ν' : Measure 𝓧 := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have this₁ : IsFiniteMeasure μ'
Tactic: have : IsFiniteMeasure μ' := μ.smul_finite (by simp [hν])
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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 μ'
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have hμν' : μ' ≪ ν'
Tactic: have hμν' : μ' ≪ ν' := hμν.smul _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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μν' : μ' ≪ ν'
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
have h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
Tactic: have h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν' :=
      Measure.rnDeriv_smul_left_of_ne_top' (μ := ν') (ν := μ) (by simp [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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
have hc : Ne (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [Measure.ae_ennreal_smul_measure_eq] at h1'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
have h1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
Tactic: have h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν' := by
      rwa [Measure.ae_ennreal_smul_measure_eq] at h1'
      simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
have h2 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
Tactic: have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
      Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by simp [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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
have h : ∀ (x : 𝓧) (h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x)
  (h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x),
  μ'.rnDeriv ν' x = μ.rnDeriv ν x
Tactic: filter_upwards [h1, h2] with x h1 h2
-- 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
⊢ μ'.rnDeriv ν' x = μ.rnDeriv ν x
have h : HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
    (HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x) =
  μ.rnDeriv ν x
Tactic: rw [h1, Pi.smul_apply, smul_eq_mul, h2]
-- 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
⊢ HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x) =
    μ.rnDeriv ν x
have h : HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (μ.rnDeriv ν x)) =
  μ.rnDeriv ν x
Tactic: simp only [inv_inv, Pi.smul_apply, smul_eq_mul]
-- 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
⊢ HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (μ.rnDeriv ν x)) =
    μ.rnDeriv ν x
have h : Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]
-- 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μν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h1_1 : μ'.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν')
h2_1 : μ.rnDeriv ν' =ᶠ[ae ν] HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν)
x : 𝓧
h1 : μ'.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹⁻¹ : ℝ≥0∞) (μ.rnDeriv ν) x
h : Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (((ν : (a : Set 𝓧) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (μ.rnDeriv ν x)) =
    μ.rnDeriv ν x
have h₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (hypothesis)
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μν' : μ' ≪ ν'
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
Tactic: have h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν := by
    have h1' : μ'.rnDeriv ν' =ᵐ[ν'] (ν univ)⁻¹ • μ.rnDeriv ν' :=
      Measure.rnDeriv_smul_left_of_ne_top' (μ := ν') (ν := μ) (by simp [hν])
    have h1 : μ'.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹ • μ.rnDeriv ν' := by
      rwa [Measure.ae_ennreal_smul_measure_eq] at h1'
      simp
    have h2 : μ.rnDeriv ν' =ᵐ[ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν :=
      Measure.rnDeriv_smul_right_of_ne_top' (μ := ν) (ν := μ) (by simp) (by simp [hν])
    filter_upwards [h1, h2] with x h1 h2
    rw [h1, Pi.smul_apply, smul_eq_mul, h2]
    simp only [inv_inv, Pi.smul_apply, smul_eq_mul]
    rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]
    · simp [hν]
    · simp
-- 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 ν
⊢ ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have rw : (ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ))⁻¹ * ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν =
  (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
Tactic: rw [integral_smul_measure, smul_eq_mul, ENNReal.toReal_inv]
-- 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 ν
⊢ (ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ))⁻¹ * ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν =
    (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have e_a : Eq (α := ℝ) (∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν) (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν)
Tactic: congr 1
-- 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 ν
⊢ Eq (α := ℝ) (∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν) (∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν)
have e_a : (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) fun (x : 𝓧) ↦ f (μ.rnDeriv ν x).toReal
Tactic: refine integral_congr_ae ?_
-- 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 ν
⊢ (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 ν
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 (hypothesis)
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 ν
⊢ ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
have h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
Tactic: have h_eq : ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν'
      = (ν.real univ)⁻¹ * ∫ x, f ((μ.rnDeriv ν x).toReal) ∂ν := by
    rw [integral_smul_measure, smul_eq_mul, ENNReal.toReal_inv]
    congr 1
    refine integral_congr_ae ?_
    filter_upwards [h_rnDeriv_eq] with x hx
    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 ∂ν
⊢ ν.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 * f (μ.real univ / ν.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
Tactic: have h : f (μ'.real univ) ≤ ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν' :=
    le_integral_rnDeriv_of_ac hf_cvx hf_cont ?_ 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 ∂ν
neg :
  ∀ (h : 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₁ : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν'
Tactic: have h : f (μ'.real univ) ≤ ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν' :=
    le_integral_rnDeriv_of_ac hf_cvx hf_cont ?_ 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 ∂ν
⊢ Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν'
have neg : Integrable (ε := ℝ) (fun (x : 𝓧) ↦ f (μ'.rnDeriv ν' x).toReal) ν
Tactic: refine Integrable.smul_measure ?_ (by simp [hν])