α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ ∫⁻ (a : α), g a ∂Measure.withDensity μ f
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
refine' le_antisymm (lintegral_withDensity_le_lintegral_mul μ f_meas g) _
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
⊢ (⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), (f * g) a ∂μ) ≤ ∫⁻ (a : α), g a ∂Measure.withDensity μ f
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
⊢ (∫⁻ (a : α), i a ∂μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
⊢ (⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => (f * g) a), ∫⁻ (a : α), g_1 a ∂μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f
refine' iSup₂_le fun i i_meas => iSup_le fun hi => _
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
⊢ (∫⁻ (a : α), i a ∂μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f
have A : (fun x => (f x)⁻¹ * i x) ≤ g := by
  intro x
  dsimp
  rw [mul_comm, ← div_eq_mul_inv]
  exact div_le_of_le_mul' (hi x)
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤
    ⨆ (_ : (fun x => (f x)⁻¹ * i x) ≤ fun a => g a), ∫⁻ (a : α), (fun x => (f x)⁻¹ * i x) a ∂Measure.withDensity μ f
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤
    ⨆ (g_1 : α → ℝ≥0∞) (_ : Measurable g_1) (_ : g_1 ≤ fun a => g a), ∫⁻ (a : α), g_1 a ∂Measure.withDensity μ f
refine' le_iSup_of_le (fun x => (f x)⁻¹ * i x) (le_iSup_of_le (f_meas.inv.mul i_meas) _)
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤ ∫⁻ (a : α), (fun x => (f x)⁻¹ * i x) a ∂Measure.withDensity μ f
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤
    ⨆ (_ : (fun x => (f x)⁻¹ * i x) ≤ fun a => g a), ∫⁻ (a : α), (fun x => (f x)⁻¹ * i x) a ∂Measure.withDensity μ f
refine' le_iSup_of_le A _
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤ ∫⁻ (a : α), (f * fun a => (f a)⁻¹ * i a) a ∂μ
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤ ∫⁻ (a : α), (fun x => (f x)⁻¹ * i x) a ∂Measure.withDensity μ f
rw [lintegral_withDensity_eq_lintegral_mul _ f_meas (f_meas.inv.mul i_meas)]
case h
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∀ᵐ (a : α) ∂μ, i a ≤ (f * fun a => (f a)⁻¹ * i a) a
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ (∫⁻ (a : α), i a ∂μ) ≤ ∫⁻ (a : α), (f * fun a => (f a)⁻¹ * i a) a ∂μ
apply lintegral_mono_ae
case h
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∀ (a : α), f a < ⊤ → i a ≤ (f * fun a => (f a)⁻¹ * i a) a
case h
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∀ᵐ (a : α) ∂μ, i a ≤ (f * fun a => (f a)⁻¹ * i a) a
filter_upwards [hf]
case h
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
case h
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
⊢ ∀ (a : α), f a < ⊤ → i a ≤ (f * fun a => (f a)⁻¹ * i a) a
intro x h'x
case h.inl
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x

case h.inr
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
case h
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
rcases eq_or_ne (f x) 0 with (hx | hx)
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
x : α
⊢ (fun x => (f x)⁻¹ * i x) x ≤ g x
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
⊢ (fun x => (f x)⁻¹ * i x) ≤ g
intro x
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
x : α
⊢ (f x)⁻¹ * i x ≤ g x
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
x : α
⊢ (fun x => (f x)⁻¹ * i x) x ≤ g x
dsimp
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
x : α
⊢ i x / f x ≤ g x
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
x : α
⊢ (f x)⁻¹ * i x ≤ g x
rw [mul_comm, ← div_eq_mul_inv]
no goals
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
x : α
⊢ i x / f x ≤ g x
exact div_le_of_le_mul' (hi x)
case h.inl
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x ≤ (fun a => (f * g) a) x
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
case h.inl
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
have := hi x
case h.inl
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x = 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
case h.inl
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x ≤ (fun a => (f * g) a) x
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
simp only [hx, MulZeroClass.zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this
no goals
case h.inl
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x = 0
this : i x = 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
simp [this]
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = (f * fun a => (f a)⁻¹ * i a) x
case h.inr
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x ≤ (f * fun a => (f a)⁻¹ * i a) x
apply le_of_eq _
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = (f * fun a => (f a)⁻¹ * i a) x
dsimp
no goals
α : Type u_1
β : Type ?u.1806740
γ : Type ?u.1806743
δ : Type ?u.1806746
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ⊤
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ fun a => (f * g) a
A : (fun x => (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ⊤
hx : f x ≠ 0
⊢ i x = f x * ((f x)⁻¹ * i x)
rw [← mul_assoc, ENNReal.mul_inv_cancel hx h'x.ne, one_mul]