α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ limsup f (Measure.ae (c • μ)) = limsup f (Measure.ae μ)
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ essSup f (c • μ) = essSup f μ
simp_rw [essSup]
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
h_smul : Measure.ae (c • μ) = Measure.ae μ
⊢ limsup f (Measure.ae (c • μ)) = limsup f (Measure.ae μ)

case h_smul
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ Measure.ae (c • μ) = Measure.ae μ
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ limsup f (Measure.ae (c • μ)) = limsup f (Measure.ae μ)
suffices h_smul : (c • μ).ae = μ.ae
case h_smul.a
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
s✝ : Set α
⊢ s✝ ∈ Measure.ae (c • μ) ↔ s✝ ∈ Measure.ae μ
case h_smul
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ Measure.ae (c • μ) = Measure.ae μ
ext1
case h_smul.a
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
s✝ : Set α
⊢ ↑↑(c • μ) (s✝ᶜ) = 0 ↔ ↑↑μ (s✝ᶜ) = 0
case h_smul.a
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
s✝ : Set α
⊢ s✝ ∈ Measure.ae (c • μ) ↔ s✝ ∈ Measure.ae μ
simp_rw [mem_ae_iff]
no goals
case h_smul.a
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
s✝ : Set α
⊢ ↑↑(c • μ) (s✝ᶜ) = 0 ↔ ↑↑μ (s✝ᶜ) = 0
simp [hc]
no goals
α : Type u_2
β : Type u_1
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
h_smul : Measure.ae (c • μ) = Measure.ae μ
⊢ limsup f (Measure.ae (c • μ)) = limsup f (Measure.ae μ)
rw [h_smul]