case mp
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (withDensity μ fun x => ↑(f x)) → AEStronglyMeasurable (fun x => ↑(f x) • g x) μ

case mpr
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ → AEStronglyMeasurable g (withDensity μ fun x => ↑(f x))
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (withDensity μ fun x => ↑(f x)) ↔ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
constructor
case mp.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
case mp
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (withDensity μ fun x => ↑(f x)) → AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
rintro ⟨g', g'meas, hg'⟩
case mp.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
case mp.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
case mp.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ (fun x => ↑(f x) • g x) =ᶠ[ae μ] fun x => ↑(f x) • g' x
case mp.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
refine' ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.stronglyMeasurable.smul g'meas, _⟩
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x

case mp.intro.intro.htc
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ ({x | f x ≠ 0}ᶜ), (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
case mp.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ (fun x => ↑(f x) • g x) =ᶠ[ae μ] fun x => ↑(f x) • g' x
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ {x | f x ≠ 0}, (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
rw [ae_restrict_iff' A]
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≠ 0} → (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
filter_upwards [hg'] with a ha h'a
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne.def, ENNReal.coe_eq_zero] using h'a
no goals
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a
rw [ha this]
no goals
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) ≠ 0
simpa only [Ne.def, ENNReal.coe_eq_zero] using h'a
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : x ∈ {x | f x ≠ 0}ᶜ
⊢ ↑(f x) • g x = ↑(f x) • g' x
case mp.intro.intro.htc
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ ({x | f x ≠ 0}ᶜ), (fun x => ↑(f x) • g x) x = (fun x => ↑(f x) • g' x) x
filter_upwards [ae_restrict_mem A.compl] with x hx
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : f x = 0
⊢ ↑(f x) • g x = ↑(f x) • g' x
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : x ∈ {x | f x ≠ 0}ᶜ
⊢ ↑(f x) • g x = ↑(f x) • g' x
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
no goals
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᶠ[ae (withDensity μ fun x => ↑(f x))] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : f x = 0
⊢ ↑(f x) • g x = ↑(f x) • g' x
simp [hx]
case mpr.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ AEStronglyMeasurable g (withDensity μ fun x => ↑(f x))
case mpr
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x => ↑(f x) • g x) μ → AEStronglyMeasurable g (withDensity μ fun x => ↑(f x))
rintro ⟨g', g'meas, hg'⟩
case mpr.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (withDensity μ fun x => ↑(f x))] fun x => (↑(f x))⁻¹ • g' x
case mpr.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ AEStronglyMeasurable g (withDensity μ fun x => ↑(f x))
refine' ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.stronglyMeasurable.smul g'meas, _⟩
case mpr.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x
case mpr.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (withDensity μ fun x => ↑(f x))] fun x => (↑(f x))⁻¹ • g' x
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x
case mpr.intro.intro
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x
filter_upwards [hg'] with x hx h'x
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x
rw [← hx, smul_smul, _root_.inv_mul_cancel, one_smul]
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0
simp only [Ne.def, ENNReal.coe_eq_zero] at h'x
no goals
case h
α : Type u_2
β : Type ?u.509907
γ : Type ?u.509910
ι : Type ?u.509913
inst✝⁴ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
f✝ g✝ : α → β
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x => ↑(f x) • g x) =ᶠ[ae μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0
simpa only [NNReal.coe_eq_zero, Ne.def] using h'x