-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- `integrableExpSet X μ` is a convex subset of `ℝ` (it is an interval). -/
lemma convex_integrableExpSet : Convex ℝ (integrableExpSet X μ)

Proof state:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ = a * t₁ + b * t₁

Tactic:
rw [← add_mul, hab, one_mul]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
wlog h_le : t₁ ≤ t₂

Result:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : ¬t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : b + a = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : ¬t₁ ≤ t₂
⊢ b • t₂ + a • t₁ ∈ integrableExpSet X μ

Tactic:
exact this ht₂ ht₁ hb ha hab (not_le.mp h_le).le

Result:
no goals

Proof state:
case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₁ + b * t₂ ≤ t₂

Tactic:
calc a * t₁ + b * t₂
_ ≤ a * t₂ + b * t₂ := by gcongr
_ = t₂ := by rw [← add_mul, hab, one_mul]

Result:
no goals

Proof state:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₂ + b * t₂ = t₂

Tactic:
rw [← add_mul, hab, one_mul]

Result:
no goals

Proof state:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
refine integrable_exp_mul_of_le_of_le ht₁ ht₂ ?_ ?_

Result:
case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a • t₁ + b • t₂

case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂

Proof state:
case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a • t₁ + b • t₂

Tactic:
simp only [smul_eq_mul]

Result:
case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a * t₁ + b * t₂

Proof state:
case refine_1
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ t₁ ≤ a * t₁ + b * t₂

Tactic:
calc t₁
_ = a * t₁ + b * t₁ := by rw [← add_mul, hab, one_mul]
_ ≤ a * t₁ + b * t₂ := by gcongr

Result:
no goals

Proof state:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : ¬t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Tactic:
rw [add_comm] at hab ⊢

Result:
case inr
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : b + a = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : Measure Ω} ⦃t₁ : ℝ⦄,
    t₁ ∈ integrableExpSet X μ →
      ∀ ⦃t₂ : ℝ⦄,
        t₂ ∈ integrableExpSet X μ →
          ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → t₁ ≤ t₂ → a • t₁ + b • t₂ ∈ integrableExpSet X μ
h_le : ¬t₁ ≤ t₂
⊢ b • t₂ + a • t₁ ∈ integrableExpSet X μ

Proof state:
case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a • t₁ + b • t₂ ≤ t₂

Tactic:
simp only [smul_eq_mul]

Result:
case refine_2
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₁ + b * t₂ ≤ t₂

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Convex ℝ (integrableExpSet X μ)

Tactic:
rintro t₁ ht₁ t₂ ht₂ a b ha hb hab

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • t₁ + b • t₂ ∈ integrableExpSet X μ

Proof state:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₁ + b * t₁ ≤ a * t₁ + b * t₂

Tactic:
gcongr

Result:
no goals

Proof state:
Ω✝ : Type u_1
m✝ : MeasurableSpace Ω✝
X✝ : Ω✝ → ℝ
μ✝ : Measure Ω✝
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t₁ : ℝ
ht₁ : t₁ ∈ integrableExpSet X μ
t₂ : ℝ
ht₂ : t₂ ∈ integrableExpSet X μ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_le : t₁ ≤ t₂
⊢ a * t₁ + b * t₂ ≤ a * t₂ + b * t₂

Tactic:
gcongr

Result:
no goals