[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : { x // x ∈ Lp E p }
⊢ ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f
[PROOFSTEP]
rw [← coeFn_le]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
have h0 := Lp.coeFn_zero E p μ
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑f → ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ ↑↑0 ≤ᵐ[μ] ↑↑f → 0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑f
⊢ ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
filter_upwards [h, h0] with _ _ h2
[GOAL]
case mpr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : ↑↑0 ≤ᵐ[μ] ↑↑f
⊢ 0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
filter_upwards [h, h0] with _ _ h2
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑↑0 a✝¹ ≤ ↑↑f a✝¹
[PROOFSTEP]
rwa [h2]
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : ↑↑0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
[PROOFSTEP]
rwa [← h2]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
⊢ CovariantClass { x // x ∈ Lp E p } { x // x ∈ Lp E p } (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine' ⟨fun f g₁ g₂ hg₁₂ => _⟩
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : g₁ ≤ g₂
⊢ f + g₁ ≤ f + g₂
[PROOFSTEP]
rw [← coeFn_le] at hg₁₂ ⊢
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
⊢ ↑↑(f + g₁) ≤ᵐ[μ] ↑↑(f + g₂)
[PROOFSTEP]
filter_upwards [coeFn_add f g₁, coeFn_add f g₂, hg₁₂] with _ h1 h2 h3
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
h2 : ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝
h3 : ↑↑g₁ a✝ ≤ ↑↑g₂ a✝
⊢ ↑↑(f + g₁) a✝ ≤ ↑↑(f + g₂) a✝
[PROOFSTEP]
rw [h1, h2, Pi.add_apply, Pi.add_apply]
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
h2 : ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝
h3 : ↑↑g₁ a✝ ≤ ↑↑g₂ a✝
⊢ ↑↑f a✝ + ↑↑g₁ a✝ ≤ ↑↑f a✝ + ↑↑g₂ a✝
[PROOFSTEP]
exact add_le_add le_rfl h3
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : f ∈ Lp E p
hg : g ∈ Lp E p
⊢ f ⊔ g ∈ Lp E p
[PROOFSTEP]
rw [mem_Lp_iff_memℒp] at *
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : Memℒp (↑f) p
hg : Memℒp (↑g) p
⊢ Memℒp (↑(f ⊔ g)) p
[PROOFSTEP]
exact (memℒp_congr_ae (AEEqFun.coeFn_sup _ _)).mpr (hf.sup hg)
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : f ∈ Lp E p
hg : g ∈ Lp E p
⊢ f ⊓ g ∈ Lp E p
[PROOFSTEP]
rw [mem_Lp_iff_memℒp] at *
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : Memℒp (↑f) p
hg : Memℒp (↑g) p
⊢ Memℒp (↑(f ⊓ g)) p
[PROOFSTEP]
exact (memℒp_congr_ae (AEEqFun.coeFn_inf _ _)).mpr (hf.inf hg)
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : |f| ≤ |g|
⊢ ‖f‖ ≤ ‖g‖
[PROOFSTEP]
rw [← coeFn_le] at hfg 
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
⊢ ‖f‖ ≤ ‖g‖
[PROOFSTEP]
simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.snorm_ne_top f) (Lp.snorm_ne_top g)]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
⊢ snorm (↑↑f) p μ ≤ snorm (↑↑g) p μ
[PROOFSTEP]
refine' snorm_mono_ae _
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
[PROOFSTEP]
filter_upwards [hfg, Lp.coeFn_abs f, Lp.coeFn_abs g] with x hx hxf hxg
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : ↑↑|f| x ≤ ↑↑|g| x
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖
[PROOFSTEP]
rw [hxf, hxg] at hx 
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : |↑↑f x| ≤ |↑↑g x|
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖
[PROOFSTEP]
exact HasSolidNorm.solid hx
