-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma withDensity_inv_same_le {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    (μ.withDensity f).withDensity f⁻¹ ≤ μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x => (f x)⁻¹) ≤ᶠ[ae μ] 1
⊢ μ.withDensity 1 ≤ μ

Tactic:
rw [withDensity_one]

Result:
no goals

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : ¬f x = ⊤
hx_zero : ¬f x = 0
⊢ f x * (f x)⁻¹ ≤ 1

Tactic:
rw [ENNReal.mul_inv_cancel hx_zero hx_top]

Result:
no goals

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ f x * (f x)⁻¹ ≤ 1

Tactic:
by_cases hx_top : f x = ∞

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : f x = ⊤
⊢ f x * (f x)⁻¹ ≤ 1

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : ¬f x = ⊤
⊢ f x * (f x)⁻¹ ≤ 1

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : ¬f x = ⊤
⊢ f x * (f x)⁻¹ ≤ 1

Tactic:
by_cases hx_zero : f x = 0

Result:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : ¬f x = ⊤
hx_zero : f x = 0
⊢ f x * (f x)⁻¹ ≤ 1

case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : ¬f x = ⊤
hx_zero : ¬f x = 0
⊢ f x * (f x)⁻¹ ≤ 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f).withDensity f⁻¹ ≤ μ

Tactic:
change (μ.withDensity f).withDensity (fun x ↦ (f x)⁻¹) ≤ μ

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ((μ.withDensity f).withDensity fun x => (f x)⁻¹) ≤ μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x => (f x)⁻¹) ≤ᶠ[ae μ] 1
⊢ μ.withDensity (f * fun x => (f x)⁻¹) ≤ μ

Tactic:
refine (withDensity_mono this).trans ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x => (f x)⁻¹) ≤ᶠ[ae μ] 1
⊢ μ.withDensity 1 ≤ μ

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : f x = ⊤
⊢ f x * (f x)⁻¹ ≤ 1

Tactic:
simp only [hx_top, ENNReal.inv_top, mul_zero, zero_le]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity (f * fun x => (f x)⁻¹) ≤ μ

Tactic:
suffices (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1 by
  refine (withDensity_mono this).trans ?_
  rw [withDensity_one]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (f * fun x => (f x)⁻¹) ≤ᶠ[ae μ] 1

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ (f * fun x => (f x)⁻¹) x ≤ 1 x

Tactic:
simp only [Pi.mul_apply, Pi.one_apply]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ f x * (f x)⁻¹ ≤ 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ((μ.withDensity f).withDensity fun x => (f x)⁻¹) ≤ μ

Tactic:
rw [← withDensity_mul₀ hf hf.inv]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity (f * fun x => (f x)⁻¹) ≤ μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (f * fun x => (f x)⁻¹) ≤ᶠ[ae μ] 1

Tactic:
filter_upwards with x

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ (f * fun x => (f x)⁻¹) x ≤ 1 x

Proof state:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
hx_top : ¬f x = ⊤
hx_zero : f x = 0
⊢ f x * (f x)⁻¹ ≤ 1

Tactic:
simp only [hx_zero, ENNReal.inv_zero, zero_mul, zero_le]

Result:
no goals