[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEMeasurable g ↔ AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEMeasurable g → AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
rintro ⟨g', g'meas, hg'⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
⊢ AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
have A : MeasurableSet {x : α | f x ≠ 0} := (hf (measurableSet_singleton 0)).compl
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ AEMeasurable fun x => ↑(f x) • g x
[PROOFSTEP]
refine' ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.smul g'meas, _⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ (fun x => ↑(f x) • g x) =ᵐ[μ] fun x => ↑(f x) • g' x
[PROOFSTEP]
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ {x | f x ≠ 0}
[GOAL]
case mp.intro.intro.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.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
[PROOFSTEP]
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg' 
[GOAL]
case mp.intro.intro.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable 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
[PROOFSTEP]
rw [ae_restrict_iff' A]
[GOAL]
case mp.intro.intro.ht
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable 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
[PROOFSTEP]
filter_upwards [hg']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ (a : α), (↑(f a) ≠ 0 → g a = g' a) → f a ≠ 0 → ↑(f a) • g a = ↑(f a) • g' a
[PROOFSTEP]
intro a ha h'a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable 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
[PROOFSTEP]
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using h'a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable 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
[PROOFSTEP]
simpa only [Ne.def, coe_eq_zero] using h'a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable 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
[PROOFSTEP]
rw [ha this]
[GOAL]
case mp.intro.intro.htc
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.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
[PROOFSTEP]
filter_upwards [ae_restrict_mem A.compl]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ (a : α), a ∈ {x | f x ≠ 0}ᶜ → ↑(f a) • g a = ↑(f a) • g' a
[PROOFSTEP]
intro x hx
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.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
[PROOFSTEP]
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx 
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[Measure.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
[PROOFSTEP]
simp [hx]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ (AEMeasurable fun x => ↑(f x) • g x) → AEMeasurable g
[PROOFSTEP]
rintro ⟨g', g'meas, hg'⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ AEMeasurable g
[PROOFSTEP]
refine' ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, _⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ g =ᵐ[Measure.withDensity μ fun x => ↑(f x)] fun x => (↑(f x))⁻¹ • g' x
[PROOFSTEP]
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x
[PROOFSTEP]
filter_upwards [hg']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
⊢ ∀ (a : α), ↑(f a) • g a = g' a → ↑(f a) ≠ 0 → g a = (↑(f a))⁻¹ • g' a
[PROOFSTEP]
intro x hx h'x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ g x = (↑(f x))⁻¹ • g' x
[PROOFSTEP]
rw [← hx, smul_smul, _root_.inv_mul_cancel, one_smul]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ↑(f x) ≠ 0
⊢ ↑(f x) ≠ 0
[PROOFSTEP]
simp only [Ne.def, coe_eq_zero] at h'x 
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace.SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x => ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0
[PROOFSTEP]
simpa only [NNReal.coe_eq_zero, Ne.def] using h'x
