case mp
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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

case mpr
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
constructor
case mp.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rintro ⟨g', g'meas, hg'⟩
case mp.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
case mp.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
refine' ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.smul g'meas, _⟩
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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

case mp.intro.intro.htc
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rw [ae_restrict_iff' A]
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro.ht
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
filter_upwards [hg']
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
intro a ha h'a
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using h'a
no goals
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rw [ha this]
no goals
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
simpa only [Ne.def, coe_eq_zero] using h'a
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mp.intro.intro.htc
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
filter_upwards [ae_restrict_mem A.compl]
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
intro x hx
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
no goals
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
simp [hx]
case mpr.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mpr
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rintro ⟨g', g'meas, hg'⟩
case mpr.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mpr.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
refine' ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, _⟩
case mpr.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mpr.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case mpr.intro.intro
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
filter_upwards [hg']
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
intro x hx h'x
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
rw [← hx, smul_smul, _root_.inv_mul_cancel, one_smul]
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
simp only [Ne.def, coe_eq_zero] at h'x
no goals
case h
α : Type u_2
β : Type ?u.28
γ : Type ?u.31
δ : Type ?u.34
m : MeasurableSpace α
μ : MeasureTheory.Measure α
E : Type u_1
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
simpa only [NNReal.coe_eq_zero, Ne.def] using h'x