internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.isFar_le
Proof state before:
case intro.intro
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝¹ : DecidableRel G✝.Adj
inst✝ : DecidableRel H✝.Adj
s t : ℕ
G H : SimpleGraph α
h : s ≤ t
S : Finset (Sym2 α)
hS1 : delFedges G S ≤ H
hS2 : card S ≤ s
⊢ IsFar G H t
Tactic:
exact ⟨S, hS1, hS2.trans h⟩
Proof state after:
no goals
Theorem: SimpleGraph.isFar_trivial
Proof state before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
⊢ card (edgeFinset G) ≤ s → IsFar G H s
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ IsFar G H s
Theorem: SimpleGraph.isFar_trivial
Proof state before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ IsFar G H s
Tactic:
refine ⟨G.edgeFinset, ?_, h⟩
Proof state after:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ delFedges G (edgeFinset G) ≤ H
Theorem: SimpleGraph.isFar_trivial
Proof state before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ delFedges G (edgeFinset G) ≤ H
Tactic:
rw [delFedges_is_sdiff,_root_.sdiff_self]
Proof state after:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ ⊥ ≤ H
Theorem: SimpleGraph.isFar_trivial
Proof state before:
α : Type u_1
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
G✝ H✝ : SimpleGraph α
inst✝² : DecidableRel G✝.Adj
inst✝¹ : DecidableRel H✝.Adj
G H : SimpleGraph α
s : ℕ
inst✝ : DecidableRel G.Adj
h : card (edgeFinset G) ≤ s
⊢ ⊥ ≤ H
Tactic:
exact bot_le
Proof state after:
no goals
Theorem: inverse_involution
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g
Tactic:
calc
  g⁻¹⁻¹ = g⁻¹⁻¹ * 1 := by rw [mul_one]
      _ = g⁻¹⁻¹ * (g⁻¹ * g) := by rw [inv_mul_self]
      _ = (g⁻¹⁻¹ * g⁻¹) * g := by rw [mul_assoc]
      _ = 1 * g := by rw [inv_mul_self]
      _ = g := by rw [one_mul]
Proof state after:
no goals
Theorem: inverse_involution
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g⁻¹⁻¹ * 1
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: inverse_involution
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ * 1 = g⁻¹⁻¹ * (g⁻¹ * g)
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: inverse_involution
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ * (g⁻¹ * g) = g⁻¹⁻¹ * g⁻¹ * g
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: inverse_involution
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ * g⁻¹ * g = 1 * g
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: inverse_involution
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ 1 * g = g
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: inverse_involution'
Proof state before:
G : Type u_1
inst✝ : Group G
g : G
⊢ g⁻¹⁻¹ = g
Tactic:
rw [←  mul_one g⁻¹⁻¹, ←  inv_mul_self g,
    ← mul_assoc, inv_mul_self g⁻¹,  one_mul]
Proof state after:
no goals
Theorem: square_eq_two_times
Proof state before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x ^ 2 = x * x
Tactic:
calc 
x^2 = Monoid.npow (Nat.succ (Nat.succ 0)) x := 
by simp [HPow.hPow, instHPow]
_ = x * (x * 1) := 
by rw [Monoid.npow_succ, Monoid.npow_succ, Monoid.npow_zero]
_ = x * x := by rw [Monoid.mul_one]
Proof state after:
no goals
Theorem: square_eq_two_times
Proof state before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x ^ 2 = Monoid.npow (Nat.succ (Nat.succ 0)) x
Tactic:
simp [HPow.hPow, instHPow]
Proof state after:
no goals
Theorem: square_eq_two_times
Proof state before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ Monoid.npow (Nat.succ (Nat.succ 0)) x = x * (x * 1)
Tactic:
rw [Monoid.npow_succ, Monoid.npow_succ, Monoid.npow_zero]
Proof state after:
no goals
Theorem: square_eq_two_times
Proof state before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x * (x * 1) = x * x
Tactic:
rw [Monoid.mul_one]
Proof state after:
no goals
Theorem: double_eq_two_additions
Proof state before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ 2 * x = x + x
Tactic:
ring
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + 2 * (x * y) + y ^ 2
Tactic:
calc 
(x + y)^2 = (x + y)*(x + y) := by rw [square_eq_two_times]
_ = x*x + y*x + (x*y + y*y) := by rw [Distrib.left_distrib,
Distrib.right_distrib, Distrib.right_distrib]
_ = x*x + x*y + x*y + y*y := by simp only [add_left_comm,
add_assoc, mul_comm]
_ = x*x + (x*y + x*y) + y*y := by simp only [add_assoc]
_ = x*x + 2*(x*y) + y*y := by rw [← double_eq_two_additions]
_ = x^2 + 2*(x*y) + y^2 := by rw [square_eq_two_times,
square_eq_two_times]
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) ^ 2 = (x + y) * (x + y)
Tactic:
rw [square_eq_two_times]
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) * (x + y) = x * x + y * x + (x * y + y * y)
Tactic:
rw [Distrib.left_distrib,
Distrib.right_distrib, Distrib.right_distrib]
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + y * x + (x * y + y * y) = x * x + x * y + x * y + y * y
Tactic:
simp only [add_left_comm,
add_assoc, mul_comm]
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + x * y + x * y + y * y = x * x + (x * y + x * y) + y * y
Tactic:
simp only [add_assoc]
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + (x * y + x * y) + y * y = x * x + 2 * (x * y) + y * y
Tactic:
rw [← double_eq_two_additions]
Proof state after:
no goals
Theorem: binomial_formula
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ x * x + 2 * (x * y) + y * y = x ^ 2 + 2 * (x * y) + y ^ 2
Tactic:
rw [square_eq_two_times,
square_eq_two_times]
Proof state after:
no goals
Theorem: binomial_formula'
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: trinomial
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ (x + y + z) ^ 3 =
    x * y * z * 6 + x * y ^ 2 * 3 + x * z ^ 2 * 3 + x ^ 2 * y * 3 + x ^ 2 * z * 3 + x ^ 3 + y * z ^ 2 * 3 +
          y ^ 2 * z * 3 +
        y ^ 3 +
      z ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: ConvexOn.add'
Proof state before:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ConvexOn 𝕜 s (f + g)
Tactic:
constructor
Proof state after:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ Convex 𝕜 s

case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
Theorem: ConvexOn.add'
Proof state before:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ Convex 𝕜 s

case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
Tactic:
exact hf.1
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
Theorem: ConvexOn.add'
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ∀ ⦃x : E⦄,
    x ∈ s →
      ∀ ⦃y : E⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
Tactic:
intro x hx y hy a b ha hb hab
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
Theorem: ConvexOn.add'
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y
Tactic:
calc
  f (a • x + b • y) + g (a • x + b • y) ≤ a • f x + b • f y + (a • g x + b • g y) :=
    add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
  _ = a • (f x + g x) + b • (f y + g y) := by rw [smul_add, smul_add, add_add_add_comm]
Proof state after:
no goals
Theorem: ConvexOn.add'
Proof state before:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.692
α : Type ?u.695
β : Type u_3
ι : Type ?u.701
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
Tactic:
rw [smul_add, smul_add, add_add_add_comm]
Proof state after:
no goals
Theorem: ConvexOn.convex_le'
Proof state before:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
⊢ Convex 𝕜 { x | x ∈ s ∧ f x ≤ r }
Tactic:
intro x hx y hy a b ha hb hab
Proof state after:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ { x | x ∈ s ∧ f x ≤ r }
Theorem: ConvexOn.convex_le'
Proof state before:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ { x | x ∈ s ∧ f x ≤ r }
Tactic:
constructor
Proof state after:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Theorem: ConvexOn.convex_le'
Proof state before:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Tactic:
{exact hf.1 hx.1 hy.1 ha hb hab}
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Theorem: ConvexOn.convex_le'
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Tactic:
{calc
  f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
  _ ≤ a • r + b • r :=
    (add_le_add (smul_le_smul_of_nonneg hx.2 ha) (smul_le_smul_of_nonneg hy.2 hb))
  _ = r := Convex.combo_self hab r
}
Proof state after:
no goals
Theorem: ConvexOn.convex_le'
Proof state before:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
Tactic:
exact hf.1 hx.1 hy.1 ha hb hab
Proof state after:
no goals
Theorem: ConvexOn.convex_le'
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Tactic:
calc
 f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
 _ ≤ a • r + b • r :=
   (add_le_add (smul_le_smul_of_nonneg hx.2 ha) (smul_le_smul_of_nonneg hy.2 hb))
 _ = r := Convex.combo_self hab r
Proof state after:
no goals
Theorem: degree_distribution
Proof state before:
V : Type
Ω : Type u_3
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
p : NNReal
hp : p ≤ 1
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
x✝ : Sort u_1
Degree : x✝
h : sorryAx (Sort u_2) true
v : V
k : ℕ
⊢ ↑↑μ {ω | sorryAx ℕ true = k} = ↑(p ^ k) * ↑(p ^ (Fintype.card V - 1 - k)) * ↑(Nat.choose (Fintype.card V - 1) k)
Tactic:
sorry
Proof state after:
no goals
Theorem: expected_degree
Proof state before:
V : Type
Ω : Type u_3
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
p : NNReal
hp : p ≤ 1
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
x✝ : Sort u_1
Degree : x✝
h : sorryAx (Sort u_2) true
v : V
⊢ ∫ (ω : Ω), sorryAx ℝ true ∂μ = (↑(Fintype.card V) - 1) * ↑p
Tactic:
sorry
Proof state after:
no goals
Theorem: bernoulli_expectation
Proof state before:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ ∫ (ω : Ω), ↑B ω ∂μ = ↑p
Tactic:
rw [←SimpleFunc.integral_eq_integral B (integrable B μ)]
Proof state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ SimpleFunc.integral μ B = ↑p
Theorem: bernoulli_expectation
Proof state before:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
B : SimpleFunc Ω ℝ
p : ℝ≥0
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
h : Bernoulli B p μ
⊢ SimpleFunc.integral μ B = ↑p
Tactic:
simp only [SimpleFunc.integral_eq, h.range, Finset.mem_singleton, zero_ne_one, smul_eq_mul,
  not_false_eq_true, Finset.sum_insert, mul_zero, Finset.sum_singleton, h.prob_1,
  ENNReal.coe_toReal, mul_one, zero_add]
Proof state after:
no goals
Theorem: edge_ind_finite_range
Proof state before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ Set.Finite (Set.range fun ω => ↑(EdgeInd' (G ω) e))
Tactic:
apply @Set.Finite.subset ℝ {0,1} _ (Set.range fun ω => (EdgeInd' (G ω) e : ℝ)) _
Proof state after:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ Set.Finite {0, 1}

V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
Theorem: edge_ind_finite_range
Proof state before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ Set.Finite {0, 1}

V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
Tactic:
simp only [Set.mem_singleton_iff, zero_ne_one, Set.finite_singleton, Set.Finite.insert]
Proof state after:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
Theorem: edge_ind_finite_range
Proof state before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => ↑(EdgeInd' (G ω) e)) ⊆ {0, 1}
Tactic:
simp [EdgeInd']
Proof state after:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => if Edge (G ω) e then 1 else 0) ⊆ {0, 1}
Theorem: edge_ind_finite_range
Proof state before:
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
⊢ (Set.range fun ω => if Edge (G ω) e then 1 else 0) ⊆ {0, 1}
Tactic:
rintro x ⟨ω, hx⟩
Proof state after:
case intro
V : Type
inst✝² : Fintype V
inst✝¹ : DecidableEq V
Ω : Sort u_1
G : Ω → SimpleGraph V
e : EdgeType V
inst✝ : (ω : Ω) → Decidable (Edge (G ω) e)
x : ℝ
ω : Ω
hx : (fun ω => if Edge (G ω) e then 1 else 0) ω = x
⊢ x ∈ {0, 1}