awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have hp1_lt : 1 < p
Tactic: have hp1_lt : 1 < p := by
    refine lt_of_le_of_ne hp1 ?_
    symm
    exact h1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have hpq : p.HolderConjugate p.conjExponent
Tactic: have hpq := Real.HolderConjugate.conjExponent hp1_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have pos : ∀ (h0 : ∫⁻ (a : α), (f + g) a ^ p ∂μ = 0),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
pos :
  ∀ (h0 : ∫⁻ (a : α), (f + g) a ^ p ∂μ = 0),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have neg : ∀ (h0 : ¬∫⁻ (a : α), (f + g) a ^ p ∂μ = 0),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: by_cases h0 : (∫⁻ a, (f + g) a ^ p ∂μ) = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hp1 : 1 ≤ p
hp_pos : 0 < p
hf_top : ∫⁻ (a : α), f a ^ p ∂μ < ∞
hg_top : ∫⁻ (a : α), g a ^ p ∂μ < ∞
h1 : ¬p = 1
hp1_lt : 1 < p
hpq : p.HolderConjugate p.conjExponent
h0 : ∫⁻ (a : α), (f + g) a ^ p ∂μ = 0
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have pos : 0 ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: rw [h0, @ENNReal.zero_rpow_of_pos (1 / p) (by simp [lt_of_lt_of_le zero_lt_one hp1])]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have inl : ∀ (hp0 : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
  (∫⁻ (a : α), HPow.hPow (β := ℝ) ((f + g) a) 0 ∂μ) ^ (1 / 0) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / 0 - 1) *
      ((∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), HPow.hPow (β := ℝ) (g a) 0 ∂μ) ^ (1 / 0))
Tactic: rcases eq_or_lt_of_le hp0 with (rfl | hp)
Cleared hypotheses: p, hp0, hp1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
inl :
  ∀ (hp0 : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
    (∫⁻ (a : α), HPow.hPow (β := ℝ) ((f + g) a) 0 ∂μ) ^ (1 / 0) ≤
      HPow.hPow (α := ℝ≥0∞) 2 (1 / 0 - 1) *
        ((∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), HPow.hPow (β := ℝ) (g a) 0 ∂μ) ^ (1 / 0))
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have inr : ∀ (hp : 0 < p),
  (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
Tactic: rcases eq_or_lt_of_le hp0 with (rfl | hp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
⊢ (∫⁻ (a : α), HPow.hPow (β := ℝ) ((f + g) a) 0 ∂μ) ^ (1 / 0) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / 0 - 1) *
      ((∫⁻ (a : α), HPow.hPow (β := ℝ) (f a) 0 ∂μ) ^ (1 / 0) + (∫⁻ (a : α), HPow.hPow (β := ℝ) (g a) 0 ∂μ) ^ (1 / 0))
have inl : 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * HAdd.hAdd (α := ℝ≥0∞) 1 1
Tactic: simp only [Pi.add_apply, rpow_zero, lintegral_one, _root_.div_zero, zero_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * HAdd.hAdd (α := ℝ≥0∞) 1 1
have inl : 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * 2
Tactic: norm_num
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * 2
have inl : 1 ≤ (HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 1)⁻¹ * 2
Tactic: rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
inl : 1 ≤ (HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 1)⁻¹ * 2
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * 2
have inl₁ : 1 ≤ HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2
Tactic: rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : LE.le (α := ℝ) 0 0
hp1 : LE.le (α := ℝ) 0 1
inl : 1 ≤ (HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 1)⁻¹ * 2
inl₁ : 1 ≤ HMul.hMul (α := ℝ≥0∞) 2⁻¹ 2
⊢ 1 ≤ HPow.hPow (α := ℝ≥0∞) (β := ℝ) 2 (-1) * 2
have inl₂ : LE.le (α := ℝ≥0∞) 1 1
Tactic: rw [rpow_neg, rpow_one, ENNReal.inv_mul_cancel two_ne_zero ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
have rw : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)
Tactic: rw [← lintegral_add_left' (hf.pow_const p)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p + g a ^ p ∂μ) ^ (1 / p)
have h₁ : ∀ (a : α), (f + g) a ^ p ≤ f a ^ p + g a ^ p
Tactic: gcongr with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanInequalities (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : ℝ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hp0 : 0 ≤ p
hp1 : p ≤ 1
hp : 0 < p
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) 2 (1 / p - 1) * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
have a : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ + ∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
Tactic: calc
    (∫⁻ a, (f + g) a ^ p ∂μ) ^ (1 / p) ≤ ((∫⁻ a, f a ^ p ∂μ) + ∫⁻ a, g a ^ p ∂μ) ^ (1 / p) := by
      rw [← lintegral_add_left' (hf.pow_const p)]
      gcongr with a
      exact rpow_add_le_add_rpow _ _ hp0 hp1
    _ ≤ (2 : ℝ≥0∞) ^ (1 / p - 1) * ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) :=
      rpow_add_le_mul_rpow_add_rpow _ _ ((one_le_div hp).2 hp1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
⊢ AEMeasurable ρ (μ.restrict s)
have hf₁ : AEMeasurable g (μ.restrict s)
Tactic: apply AEMeasurable.ennreal_ofReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hρ_ae : AEMeasurable ρ (μ.restrict s)
Tactic: have hρ_ae : AEMeasurable ρ (μ.restrict s) := by
    apply AEMeasurable.ennreal_ofReal
    exact hg.aestronglyMeasurable.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
Tactic: have hρ_top : ∀ᵐ x ∂μ.restrict s, ρ x < ⊤ := by simp [ρ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
⊢ (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
have apply : ∀ (x : α), 0 ≤ g x → (fun (x : α) ↦ (ρ x).toReal) x = g x
Tactic: apply hg0.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
Tactic: have h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g := by
    apply hg0.mono
    intro x hx
    simpa [ρ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ)
have h : (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ (ρ a).toReal * f a
Tactic: apply MeasureTheory.integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) (fun (a : α) ↦ f a * g a) fun (a : α) ↦ (ρ a).toReal * f a
have h : ∀ (x : α),
  (fun (x : α) ↦ (ρ x).toReal) x = g x →
    Eq (α := ℝ) ((fun (a : α) ↦ f a * g a) x) ((fun (a : α) ↦ (ρ a).toReal * f a) x)
Tactic: apply h_toReal_ae.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ) (∫ (x : α) in s, f x ∂ν)
have h : Eq (α := ℝ) (∫ (x : α) in s, f x ∂μ.withDensity fun (x : α) ↦ ρ x) (∫ (x : α) in s, (ρ x).toReal • f x ∂μ)
Tactic: have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
have _ : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ)
Tactic: calc
      _ = ∫ x in s, (ρ x).toReal * f x ∂μ := by
        apply MeasureTheory.integral_congr_ae
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      _ = _ := by
        have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
        simp [ν, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
_ : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
have _₁ : Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal * f x ∂μ) (∫ (x : α) in s, f x ∂ν)
Tactic: calc
      _ = ∫ x in s, (ρ x).toReal * f x ∂μ := by
        apply MeasureTheory.integral_congr_ae
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      _ = _ := by
        have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
        simp [ν, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
Tactic: have heq : ∫ x in s, f x * g x ∂μ = ∫ x in s, f x ∂ν := by
    calc
      _ = ∫ x in s, (ρ x).toReal * f x ∂μ := by
        apply MeasureTheory.integral_congr_ae
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      _ = _ := by
        have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
        simp [ν, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
have h : Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
  (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
Tactic: have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀
      hρ_ae hρ_top (fun _ ↦ (1 : ℝ)) hs_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
h :
  Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, (ρ x).toReal ∂μ)
have rw : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (a : α) in s, g a ∂μ)
Tactic: rw [integral_congr_ae h_toReal_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
h :
  Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
have _ : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, (ρ x).toReal ∂μ)
Tactic: calc
      _ = ∫ x in s, (ρ x).toReal ∂μ := by rw [integral_congr_ae h_toReal_ae]
      _ = _ := by simp [ν, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
h :
  Eq (α := ℝ) (∫ (x : α) in s, (fun (x : α) ↦ (1 : ℝ)) x ∂μ.withDensity fun (x : α) ↦ ρ x)
    (∫ (x : α) in s, HSMul.hSMul (β := ℝ) (ρ x).toReal ((fun (x : α) ↦ (1 : ℝ)) x) ∂μ)
_ : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, (ρ x).toReal ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
have _₁ : Eq (α := ℝ) (∫ (x : α) in s, (ρ x).toReal ∂μ) (∫ (x : α) in s, 1 ∂ν)
Tactic: calc
      _ = ∫ x in s, (ρ x).toReal ∂μ := by rw [integral_congr_ae h_toReal_ae]
      _ = _ := by simp [ν, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.MeanValue (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : (x : α) → ENNReal := fun (x : α) ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun (x : α) ↦ (ρ x).toReal) =ᶠ[ae (μ.restrict s)] g
heq : Eq (α := ℝ) (∫ (x : α) in s, f x * g x ∂μ) (∫ (x : α) in s, f x ∂ν)
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
have hg1 : Eq (α := ℝ) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, 1 ∂ν)
Tactic: have hg1 : ∫ x in s, g x ∂μ = ∫ x in s, (1 : ℝ) ∂ν := by
    have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀
      hρ_ae hρ_top (fun _ ↦ (1 : ℝ)) hs_meas
    calc
      _ = ∫ x in s, (ρ x).toReal ∂μ := by rw [integral_congr_ae h_toReal_ae]
      _ = _ := by simp [ν, h]