α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
⊢ (if p ∈ Set.Ioo 0 1 then 2 ^ (1 / ENNReal.toReal p - 1) else 1) < ⊤
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
⊢ LpAddConst p < ⊤
rw [LpAddConst]
case inl
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / ENNReal.toReal p - 1) < ⊤

case inr
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : ¬p ∈ Set.Ioo 0 1
⊢ 1 < ⊤
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
⊢ (if p ∈ Set.Ioo 0 1 then 2 ^ (1 / ENNReal.toReal p - 1) else 1) < ⊤
split_ifs with h
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ 1 / ENNReal.toReal p - 1
case inl
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / ENNReal.toReal p - 1) < ⊤
apply ENNReal.rpow_lt_top_of_nonneg _ ENNReal.two_ne_top
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 1 ≤ (ENNReal.toReal p)⁻¹
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ 1 / ENNReal.toReal p - 1
simp only [one_div, sub_nonneg]
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ ENNReal.toReal p ≤ 1
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 1 ≤ (ENNReal.toReal p)⁻¹
apply one_le_inv (ENNReal.toReal_pos h.1.ne' (h.2.trans ENNReal.one_lt_top).ne)
no goals
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ ENNReal.toReal p ≤ 1
simpa using ENNReal.toReal_mono ENNReal.one_ne_top h.2.le
no goals
case inr
α : Type ?u.3022640
E : Type ?u.3022643
F : Type ?u.3022646
G : Type ?u.3022649
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
h : ¬p ∈ Set.Ioo 0 1
⊢ 1 < ⊤
exact ENNReal.one_lt_top