case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ Memℒp (↑f) p

case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
⊢ Memℒp (↑f) p
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
⊢ Memℒp (↑f) p
by_cases hp0 : p = 0
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp (↑f) p

case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ Memℒp (↑f) p
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
⊢ Memℒp (↑f) p
by_cases hp_top : p = ∞
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm (↑f) p μ < ⊤
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ Memℒp (↑f) p
refine' ⟨f.aestronglyMeasurable, _⟩
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y})) ^ (1 / ENNReal.toReal p) < ⊤
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ snorm (↑f) p μ < ⊤
rw [snorm_eq_snorm' hp0 hp_top, f.snorm'_eq]
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
⊢ ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∑ y in SimpleFunc.range f, ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y})) ^ (1 / ENNReal.toReal p) < ⊤
refine' ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top_iff.mpr fun y _ => _).ne
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
hy0 : y = 0
⊢ ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤

case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
hy0 : ¬y = 0
⊢ ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
⊢ ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
by_cases hy0 : y = 0
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ AEStronglyMeasurable (↑f) μ
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ Memℒp (↑f) p
rw [hp0, memℒp_zero_iff_aestronglyMeasurable]
no goals
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ AEStronglyMeasurable (↑f) μ
exact f.aestronglyMeasurable
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp ↑f ⊤
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp (↑f) p
rw [hp_top]
no goals
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ Memℒp ↑f ⊤
exact memℒp_top f μ
no goals
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ 0 ≤ 1 / ENNReal.toReal p
simp
no goals
case pos
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
hy0 : y = 0
⊢ ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
simp [hy0, ENNReal.toReal_pos hp0 hp_top]
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
hy0 : ¬y = 0
⊢ ↑‖y‖₊ ^ ENNReal.toReal p ≠ ⊤
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
hy0 : ¬y = 0
⊢ ↑‖y‖₊ ^ ENNReal.toReal p * ↑↑μ (↑f ⁻¹' {y}) < ⊤
refine' ENNReal.mul_lt_top _ (hf y hy0).ne
no goals
case neg
α : Type u_1
β : Type ?u.1422783
ι : Type ?u.1422786
E : Type u_2
F : Type ?u.1422792
𝕜 : Type ?u.1422795
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
p✝ p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → ↑↑μ (↑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ SimpleFunc.range f
hy0 : ¬y = 0
⊢ ↑‖y‖₊ ^ ENNReal.toReal p ≠ ⊤
exact (ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top).ne