mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ s.indicator (f - g) = f - g

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
⊢ eLpNorm 0 p μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
⊢ eLpNorm 0 p μ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
q : ℝ
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : MeasurableSpace α
f : α → ε
hq_pos : 0 < q
⊢ eLpNorm' f q 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : MeasurableSpace α
f : α → ε
⊢ eLpNorm' f 0 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
q : ℝ
ε : Type u_7
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : MeasurableSpace α
f : α → ε
hq_neg : q < 0
⊢ eLpNorm' f q 0 = ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst✝ : ENorm ε
f : α → ε
⊢ eLpNormEssSup f 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ essSup (fun x ↦ ↑(c * ‖g x‖₊)) μ = essSup (fun x ↦ ↑c * ‖g x‖ₑ) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst✝ : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝² : Fintype ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : Fintype ι'
f : ι' ≃ ι
⊢ Measure.map (⇑(MeasurableEquiv.piCongrLeft α f)) (Measure.pi fun i' ↦ μ (f i')) = Measure.pi μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst✝ : ENorm ε
f : α → ε
⊢ eLpNorm f p 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ MemLp f p 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
q : ℝ
μ : Measure α
⊢ eLpNorm' (-f) q μ = eLpNorm' f q μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (f - g) p μ = eLpNorm (g - f) p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ eLpNorm (-f) p μ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ 0 ≤ 1 / q

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
hq_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : ENorm ε
c : ε
hq_pos : 0 < q
⊢ eLpNorm' (fun x ↦ c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ μ Set.univ ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
hp_cancel : q * (1 / q) = 1
⊢ ‖c‖ₑ ^ (q * (1 / q)) = ‖c‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst✝ : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : IsFiniteMeasure μ
c : F
hc_ne_zero : c ≠ 0
hq_ne_zero : q ≠ 0
⊢ eLpNorm' (fun x ↦ c) q μ = ‖c‖ₑ * μ Set.univ ^ (1 / q)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ Measure.map (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ)) (Measure.pi fun i ↦ (μ i).prod (ν i)) =
    (Measure.pi fun i ↦ μ i).prod (Measure.pi fun i ↦ ν i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ε
hμ : μ ≠ 0
⊢ eLpNormEssSup (fun x ↦ c) μ = ‖c‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
c : ε
hq_pos : 0 < q
inst✝ : IsProbabilityMeasure μ
⊢ eLpNorm' (fun x ↦ c) q μ = ‖c‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
hμ : μ ≠ 0
⊢ eLpNorm (fun x ↦ c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
h_top : p ≠ ∞
⊢ eLpNorm (fun x ↦ c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
c : 𝕜
x✝ : α
⊢ ‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup F
f : α → F
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 F
inst✝ : IsBoundedSMul 𝕜 F
c : 𝕜
x✝ : α
⊢ ‖(c • f) x✝‖₊ ≤ ‖c‖₊ * ‖f x✝‖₊

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_3
inst✝⁴ : NormedRing 𝕜
ε : Type u_4
inst✝³ : TopologicalSpace ε
inst✝² : ESeminormedAddMonoid ε
inst✝¹ : SMul 𝕜 ε
inst✝ : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
x✝ : α
⊢ ‖(c • f) x✝‖ₑ ≤ ‖c‖ₑ * ‖f x✝‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
⊢ eLpNormEssSup (c • f) μ = ‖c‖ₑ * eLpNormEssSup f μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
⊢ Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm)
      ((Measure.pi fun i ↦ μ (Sum.inl i)).prod (Measure.pi fun i ↦ μ (Sum.inr i))) =
    Measure.pi μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: α : Type u_1
F : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : α → F
⊢ eLpNorm (n • f) p μ = ↑n * eLpNorm f p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_7
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
⊢ 0 ≤ (z - y) / (z - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
⊢ 0 ≤ (y - x) / (z - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
hc : c < 0
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ ↑c * eLpNorm g p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hp : 0 < p.toReal
hμ : ¬μ = 0
hc : ¬‖c‖ₑ = 0
hμ_ne_top : μ Set.univ ≠ ∞
⊢ μ Set.univ ^ p.toReal⁻¹ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
⊢ MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove α i)) (Measure.pi μ)
    ((μ i).prod (Measure.pi fun j ↦ μ (i.succAbove j)))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
c : ε''
hc' : ‖c‖ₑ ≠ ∞
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ eLpNorm (fun x ↦ c) p μ < ∞ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst✝³ : TopologicalSpace ε'
inst✝² : ContinuousENorm ε'
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : α → F
c : ℝ≥0
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ eLpNorm g p μ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
c : F
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ eLpNorm (fun x ↦ c) p μ < ∞ ↔ c = 0 ∨ μ Set.univ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
⊢ eLpNorm g p μ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : α → E
g : α → F
c : ℝ
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
⊢ eLpNorm g p μ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
e : ((i : ι) → X i) ≃ᵐ X default := MeasurableEquiv.piUnique X
⊢ (piPremeasure fun i ↦ (μ i).toOuterMeasure) = ⇑(Measure.map (⇑e.symm) (μ default))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
inst✝ : IsFiniteMeasure μ
⊢ MemLp (fun x ↦ c) p μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConcaveOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε' : Type u_7
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
c : ε'
hc : ‖c‖ₑ ≠ ∞
⊢ eLpNorm (fun x ↦ c) ∞ μ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
X : ι → Type u_4
inst✝ : Unique ι
m : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
⊢ Measure.map (⇑(MeasurableEquiv.piUnique X)) (Measure.pi μ) = μ default

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
p : ℝ≥0∞
c : ε''
hc : ‖c‖ₑ ≠ ∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
⊢ 0 < (z - y) / (z - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
ha : 0 < (z - y) / (z - x)
⊢ 0 < (y - x) / (z - x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ ↔ c = 0 ∨ μ Set.univ < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : 0 < y - x
hyz : 0 < z - y
hxz : 0 < z - x
hxz' : x ≠ z
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
⊢ (z - y) / (z - x) + (y - x) / (z - x) = 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ eLpNorm' f q μ ≤ eLpNorm' g q μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Fin 2 → Type u
m : (i : Fin 2) → MeasurableSpace (α i)
μ : (i : Fin 2) → Measure (α i)
inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ) ((μ 0).prod (μ 1))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: α : Type u
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun x ↦ μ) (μ.prod μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
⊢ MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) (Measure.pi μ) (Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
x : α
hx : ‖f x‖ₑ = ‖g x‖ₑ
⊢ (fun x ↦ ‖f x‖ₑ ^ q) x = (fun x ↦ ‖g x‖ₑ ^ q) x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
by

Goal state after: