α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
hg : AEMeasurable g
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
hg : AEMeasurable g
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
let f' := hf.mk f
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
hg : AEMeasurable g
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
this : Measure.withDensity μ f = Measure.withDensity μ f'
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
hg : AEMeasurable g
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
have : μ.withDensity f = μ.withDensity f' := withDensity_congr_ae hf.ae_eq_mk
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f') = ∫⁻ (a : α), (f * g) a ∂μ
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
hg : AEMeasurable g
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
this : Measure.withDensity μ f = Measure.withDensity μ f'
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f) = ∫⁻ (a : α), (f * g) a ∂μ
rw [this] at hg⊢
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f') = ∫⁻ (a : α), (f * g) a ∂μ
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
⊢ (∫⁻ (a : α), g a ∂Measure.withDensity μ f') = ∫⁻ (a : α), (f * g) a ∂μ
let g' := hg.mk g
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (fun a => (f' * g') a) =ᵐ[μ] fun a => (f' * g) a
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (∫⁻ (a : α), (f' * g') a ∂μ) = ∫⁻ (a : α), (f' * g) a ∂μ
apply lintegral_congr_ae
case h.ht
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f' x ≠ 0}, (fun a => (f' * g') a) x = (fun a => (f' * g) a) x

case h.htc
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ ({x | f' x ≠ 0}ᶜ), (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (fun a => (f' * g') a) =ᵐ[μ] fun a => (f' * g) a
apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
case h.ht
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : g =ᵐ[Measure.withDensity μ f'] AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f' x ≠ 0}, (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
case h.ht
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f' x ≠ 0}, (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
have Z := hg.ae_eq_mk
case h.ht
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂Measure.restrict μ {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f' x ≠ 0}, (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
case h.ht
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : g =ᵐ[Measure.withDensity μ f'] AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f' x ≠ 0}, (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂Measure.restrict μ {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ (a : α),
    g a = AEMeasurable.mk g hg a → (AEMeasurable.mk f hf * AEMeasurable.mk g hg) a = (AEMeasurable.mk f hf * g) a
case h.ht
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂Measure.restrict μ {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f' x ≠ 0}, (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
filter_upwards [Z]
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂Measure.restrict μ {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
x : α
hx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf * AEMeasurable.mk g hg) x = (AEMeasurable.mk f hf * g) x
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂Measure.restrict μ {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ (a : α),
    g a = AEMeasurable.mk g hg a → (AEMeasurable.mk f hf * AEMeasurable.mk g hg) a = (AEMeasurable.mk f hf * g) a
intro x hx
no goals
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂Measure.restrict μ {x | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
x : α
hx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf * AEMeasurable.mk g hg) x = (AEMeasurable.mk f hf * g) x
simp only [hx, Pi.mul_apply]
case h.htc
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ ({x | f' x ≠ 0}ᶜ), (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
case h.htc
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ ({x | f' x ≠ 0}ᶜ), (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
have M : MeasurableSet ({ x : α | f' x ≠ 0 }ᶜ) :=
  (hf.measurable_mk (measurableSet_singleton 0).compl).compl
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
⊢ ∀ (a : α),
    a ∈ {x | AEMeasurable.mk f hf x ≠ 0}ᶜ →
      (AEMeasurable.mk f hf * AEMeasurable.mk g hg) a = (AEMeasurable.mk f hf * g) a
case h.htc
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ ({x | f' x ≠ 0}ᶜ), (fun a => (f' * g') a) x = (fun a => (f' * g) a) x
filter_upwards [ae_restrict_mem M]
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
x : α
hx : x ∈ {x | AEMeasurable.mk f hf x ≠ 0}ᶜ
⊢ (AEMeasurable.mk f hf * AEMeasurable.mk g hg) x = (AEMeasurable.mk f hf * g) x
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
⊢ ∀ (a : α),
    a ∈ {x | AEMeasurable.mk f hf x ≠ 0}ᶜ →
      (AEMeasurable.mk f hf * AEMeasurable.mk g hg) a = (AEMeasurable.mk f hf * g) a
intro x hx
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
x : α
hx : AEMeasurable.mk f hf x = 0
⊢ (AEMeasurable.mk f hf * AEMeasurable.mk g hg) x = (AEMeasurable.mk f hf * g) x
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
x : α
hx : x ∈ {x | AEMeasurable.mk f hf x ≠ 0}ᶜ
⊢ (AEMeasurable.mk f hf * AEMeasurable.mk g hg) x = (AEMeasurable.mk f hf * g) x
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
no goals
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet ({x | f' x ≠ 0}ᶜ)
x : α
hx : AEMeasurable.mk f hf x = 0
⊢ (AEMeasurable.mk f hf * AEMeasurable.mk g hg) x = (AEMeasurable.mk f hf * g) x
simp only [hx, MulZeroClass.zero_mul, Pi.mul_apply]
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (fun a => (f' * g) a) =ᵐ[μ] fun a => (f * g) a
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (∫⁻ (a : α), (f' * g) a ∂μ) = ∫⁻ (a : α), (f * g) a ∂μ
apply lintegral_congr_ae
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ (a : α), f a = AEMeasurable.mk f hf a → (AEMeasurable.mk f hf * g) a = (f * g) a
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ (fun a => (f' * g) a) =ᵐ[μ] fun a => (f * g) a
filter_upwards [hf.ae_eq_mk]
case h
α : Type u_1
β : Type ?u.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
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.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ (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.1801681
γ : Type ?u.1801684
δ : Type ?u.1801687
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g
this : Measure.withDensity μ f = Measure.withDensity μ f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ (AEMeasurable.mk f hf * g) x = (f * g) x
simp only [hx, Pi.mul_apply]