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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᵐ[μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ

Tactic:
have hg_mk_f_co : IsCoboundedUnder (· ≤ ·) (ae μ) ((hg.mk g) ∘ f) := by
    simpa [IsCoboundedUnder, ← map_congr h_eq]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : ConditionallyCompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
inst✝⁴ : MeasurableSpace β
inst✝³ : TopologicalSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : OrderClosedTopology β
inst✝ : OpensMeasurableSpace β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
hg_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hgf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hgf_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (g ∘ f)
hg_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) g
hg_mk_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
hg_mk_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae (Measure.map f μ)) (AEMeasurable.mk g hg)
h_eq : g ∘ f =ᵐ[μ] AEMeasurable.mk g hg ∘ f
hg_mk_f : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
hg_mk_f_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) (ae μ) (AEMeasurable.mk g hg ∘ f)
⊢ essSup g (Measure.map f μ) = essSup (g ∘ f) μ
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case neg.h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ 0

pp: case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ ⊤

Tactic:
· rwa [← Measure.count_eq_zero_iff] at hst

Goal state after:
case neg.ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : ¬s ∩ t = ∅
⊢ Measure.count (s ∩ t) ≠ ⊤
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : ∅.Finite
hst : Disjoint ∅ ∅
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ + (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ = (uniformOn (∅ ∪ ∅)) u

pp: case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

pp: case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

pp: case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u

Tactic:
· simp

Goal state after:
case inl.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
t u : Set Ω
ht : t.Finite
hs : ∅.Finite
hst : Disjoint ∅ t
ht' : t.Nonempty
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ t)) ∅ + (uniformOn t) u * (uniformOn (∅ ∪ t)) t = (uniformOn (∅ ∪ t)) u

case inr.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : ∅.Finite
hst : Disjoint s ∅
⊢ (uniformOn s) u * (uniformOn (s ∪ ∅)) s + (uniformOn ∅) u * (uniformOn (s ∪ ∅)) ∅ = (uniformOn (s ∪ ∅)) u

case inr.inr
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
ht : t.Finite
hst : Disjoint s t
hs' : s.Nonempty
ht' : t.Nonempty
⊢ (uniformOn s) u * (uniformOn (s ∪ t)) s + (uniformOn t) u * (uniformOn (s ∪ t)) t = (uniformOn (s ∪ t)) u
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ (μ i) (update (fun j ↦ univ) i s i) = (μ i) s

pp: case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x) = ∏ j ∈ Finset.univ.erase i, (μ j) univ

Tactic:
· simp

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_3
inst✝³ : Fintype ι
inst✝² : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
⊢ ∏ x ∈ Finset.univ.erase i, (μ x) (update (fun j ↦ univ) i s x) = ∏ j ∈ Finset.univ.erase i, (μ j) univ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ε = ∞
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
have : (0 : ℝ≥0∞) ^ p.toReal = 0 := by
      rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
    simp [h, this, hmeas_top]

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
← lintegral_indicator hs

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (a : α), s.indicator (fun x ↦ ‖f x‖ₑ ^ p.toReal) a ∂μ) ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
⊢ eLpNormEssSup (s.indicator fun x ↦ c) 0 ≤ ‖c‖ₑ

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμ0 : μ ≠ 0
⊢ eLpNormEssSup (s.indicator fun x ↦ c) μ ≤ ‖c‖ₑ

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
s : Set α
c : ε
hμ0 : μ ≠ 0
⊢ eLpNormEssSup (s.indicator fun x ↦ c) μ ≤ ‖c‖ₑ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
⊢ eLpNorm (s.indicator fun x ↦ c) 0 μ ≤ ‖c‖ₑ * μ s ^ (1 / ENNReal.toReal 0)

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
c : ε
s : Set α
p : ℝ≥0∞
hp : p ≠ 0
⊢ eLpNorm (s.indicator fun x ↦ c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁵ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝³ : ∀ (i : ι), SigmaFinite (μ i)
inst✝² : (i : ι) → Group (α i)
inst✝¹ : ∀ (i : ι), MeasurableMul (α i)
inst✝ : ∀ (i : ι), (μ i).IsMulLeftInvariant
⊢ (Measure.pi μ).IsMulLeftInvariant

Tactic:
refine ⟨fun v => (pi_eq fun s hs => ?_).symm⟩
  rw [map_apply (measurable_const_mul _) (MeasurableSet.univ_pi hs),
    show (v * ·) ⁻¹' univ.pi s = univ.pi fun i => (v i * ·) ⁻¹' s i by rfl, pi_pi]
  simp_rw [measure_preimage_mul]

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

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

pp: case inr
α : 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 α
hc : c ≠ 0
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
· simp

Goal state after:
case inr
α : 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 α
hc : c ≠ 0
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ
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 : ℝ
hc : c < 0
p : ℝ≥0∞
h : f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
simp [eLpNorm_congr_ae h.1, eLpNorm_congr_ae h.2]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (x : α) in s, ↑C ^ p.toReal ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
← lintegral_indicator hs

Goal state after:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

Tactic:
simp only [eLpNorm]
  split_ifs
  · exact le_rfl
  · exact eLpNormEssSup_mono_enorm_ae h
  · exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h

Goal state after:
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
⊢ p⁻¹ + q⁻¹ < ∞ + ∞

Tactic:
by simp [hp, hq, pos_iff_ne_zero]

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

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂0, ‖f x‖ₑ ≤ C
⊢ eLpNorm f p 0 ≤ C • 0 Set.univ ^ p.toReal⁻¹

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
⊢ eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: case mp
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p = ∞ → q = 1

pp: case mpr
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q = 1 → p = ∞

Tactic:
· rintro rfl
    rw [← inv_inv q, ← one_sub_inv ∞ q]
    simp

Goal state after:
case mpr
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ q = 1 → p = ∞
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / p < log (1 + s)

Tactic:
← div_lt_div_iff_of_pos_right hs'

Goal state after:
case inr.inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + p * s) / p / s < log (1 + s) / s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
s : ℝ
hs : -1 ≤ s
hp : 1 ≤ 1
⊢ 1 + 1 * s ≤ (1 + s) ^ 1

pp: case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p

Tactic:
· simp

Goal state after:
case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ 1 + p * s ≤ (1 + s) ^ p
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x : 𝕜
ha : a ∈ s
hx : x ∈ s
hxa : x ≠ a
hy : x ∈ s
hya : x ≠ a
hxy : x ≤ x
⊢ (f x - f a) / (x - a) ≤ (f x - f a) / (x - a)

pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
a x y : 𝕜
ha : a ∈ s
hx : x ∈ s
hy : y ∈ s
hxa : x ≠ a
hya : y ≠ a
hxy✝ : x ≤ y
hxy : x < y
⊢ (f x - f a) / (x - a) ≤ (f y - f a) / (y - a)
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) < log (1 + p * s) / p

Tactic:
← div_lt_div_iff_of_pos_right hs'

Goal state after:
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp1 : 0 < p
hp2 : p < 1
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : 0 < s
⊢ log (1 + s) / s < log (1 + p * s) / p / s
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm f p (0 • μ) ≤ 0 ^ (1 / p).toReal • eLpNorm f p μ

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
f : α → ε
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
c : ℝ≥0∞
f : α → ε
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: p : ℝ≥0
hp : 1 < p
⊢ ↑p.conjExponent = (↑p).conjExponent

Tactic:
NNReal.conjExponent,

Goal state after:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = (↑p).conjExponent
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inl
s : ℝ
hs : -1 ≤ s
hp1 : 0 ≤ 0
hp2 : 0 ≤ 1
⊢ (1 + s) ^ 0 ≤ 1 + 0 * s

pp: case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
· simp

Goal state after:
case inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2 : p ≤ 1
hp1 : 0 < p
⊢ (1 + s) ^ p ≤ 1 + p * s
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: case inr.inl
s : ℝ
hs : -1 ≤ s
hp1✝ : 0 ≤ 1
hp2 : 1 ≤ 1
hp1 : 0 < 1
⊢ (1 + s) ^ 1 ≤ 1 + 1 * s

pp: case inr.inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s

Tactic:
· simp

Goal state after:
case inr.inr
s : ℝ
hs : -1 ≤ s
p : ℝ
hp1✝ : 0 ≤ p
hp2✝ : p ≤ 1
hp1 : 0 < p
hp2 : p < 1
⊢ (1 + s) ^ p ≤ 1 + p * s
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inl
hp : 1 ≤ 1
this : 1 ≠ 0
⊢ 1 + (1 - 1)⁻¹ = (1⁻¹ - 1⁻¹)⁻¹

pp: case inr
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
· simp

Goal state after:
case inr
p : ℝ≥0∞
hp : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Module: Mathlib.Data.Real.ConjExponents

Goal state before:
pp: case inr.inl
hp : 1 ≤ ∞
this : ∞ ≠ 0
hp₁ : 1 < ∞
⊢ 1 + (∞ - 1)⁻¹ = (1⁻¹ - ∞⁻¹)⁻¹

pp: case inr.inr
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹

Tactic:
· simp

Goal state after:
case inr.inr
p : ℝ≥0∞
hp✝ : 1 ≤ p
this : p ≠ 0
hp₁ : 1 < p
hp : p ≠ ∞
⊢ 1 + (p - 1)⁻¹ = (1⁻¹ - p⁻¹)⁻¹
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case inl
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f 0 μ < ∞

pp: case inr
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
⊢ eLpNorm f p μ < ∞

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
⊢ eLpNorm f p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
hp,

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ eLpNorm g ∞ (Measure.map f μ) = eLpNorm (g ∘ f) ∞ μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ ‖f n x‖ₑ ^ p.toReal) atTop < ∞

Tactic:
simp only [hp0, ENNReal.rpow_zero]

Goal state after:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n ↦ 1) atTop < ∞
Module: Mathlib.Algebra.Order.Monovary

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ Monovary f (⇑OrderDual.toDual ∘ g) ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rw [monovary_iff_smul_rearrangement]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : IsStrictOrderedModule α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι),
      f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤
        f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔
    ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inl
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

pp: case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
· simp

Goal state after:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∀ i ∈ {i ∈ s | w i ≠ 0}, 0 < w i

Tactic:
by grind

Goal state after:
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case inl
a b : ℝ≥0∞
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

pp: case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
· simp

Goal state after:
case inr
p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : ι → ℝ := fun i ↦ p i / (1 - p i₀)
⊢ (∑ x ∈ insert i₀ s, p x - p i₀) / (1 - p i₀) = 1

Tactic:
hp,

Goal state after:
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
f : ι → α → ℝ≥0∞
i₀ : ι
s : Finset ι
hi₀ : i₀ ∉ s
ih :
  (∀ i ∈ s, AEMeasurable (f i) μ) →
    ∀ {p : ι → ℝ},
      ∑ i ∈ s, p i = 1 →
        (∀ i ∈ s, 0 ≤ p i) → ∫⁻ (a : α), ∏ i ∈ s, f i a ^ p i ∂μ ≤ ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
hf : ∀ i ∈ insert i₀ s, AEMeasurable (f i) μ
p : ι → ℝ
hp : ∑ i ∈ insert i₀ s, p i = 1
h2p : ∀ i ∈ insert i₀ s, 0 ≤ p i
h2i₀ : p i₀ ≠ 1
hpi₀ : 0 ≤ 1 - p i₀
h2pi₀ : 1 - p i₀ ≠ 0
q : ι → ℝ := fun i ↦ p i / (1 - p i₀)
⊢ (1 - p i₀) / (1 - p i₀) = 1
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case left
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ 0 < (ENNReal.ofReal p)⁻¹

pp: case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1

Tactic:
· simp

Goal state after:
case right
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1