α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
let f' := hf.mk f
no goals
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
calc
  (∫⁻ a, g a ∂μ.withDensity f) = ∫⁻ a, g a ∂μ.withDensity f' := by
    rw [withDensity_congr_ae hf.ae_eq_mk]
  _ = ∫⁻ a, (f' * g) a ∂μ := by
    apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
    filter_upwards [h'f, hf.ae_eq_mk]
    intro x hx h'x
    rwa [← h'x]
  _ = ∫⁻ a, (f * g) a ∂μ := by
    apply lintegral_congr_ae
    filter_upwards [hf.ae_eq_mk]
    intro x hx
    simp only [hx, Pi.mul_apply]
no goals
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), g a ∂Measure.withDensity μ f'
rw [withDensity_congr_ae hf.ae_eq_mk]
case hf
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ, AEMeasurable.mk f hf x < ⊤
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f') = ∫⁻ (a : α), (f' * g) a ∂μ
apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a < ⊤ → f a = AEMeasurable.mk f hf a → AEMeasurable.mk f hf a < ⊤
case hf
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ, AEMeasurable.mk f hf x < ⊤
filter_upwards [h'f, hf.ae_eq_mk]
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x < ⊤
h'x : f x = AEMeasurable.mk f hf x
⊢ AEMeasurable.mk f hf x < ⊤
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a < ⊤ → f a = AEMeasurable.mk f hf a → AEMeasurable.mk f hf a < ⊤
intro x hx h'x
no goals
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x < ⊤
h'x : f x = AEMeasurable.mk f hf x
⊢ AEMeasurable.mk f hf x < ⊤
rwa [← h'x]
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (fun a => (f' * g) a) =ᵐ[μ] fun a => (f * g) a
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), (f' * g) a ∂μ) = ∫⁻ (a : α), (f * g) a ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a = AEMeasurable.mk f hf a → (AEMeasurable.mk f hf * g) a = (f * g) a
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (fun a => (f' * g) a) =ᵐ[μ] fun a => (f * g) a
filter_upwards [hf.ae_eq_mk]
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (AEMeasurable.mk f hf * g) x = (f * g) x
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∀ (a : α), f a = AEMeasurable.mk f hf a → (AEMeasurable.mk f hf * g) a = (f * g) a
intro x hx
no goals
case h
α : Type u_1
β : Type ?u.1811893
γ : Type ?u.1811896
δ : Type ?u.1811899
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (AEMeasurable.mk f hf * g) x = (f * g) x
simp only [hx, Pi.mul_apply]