1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101

import algebra.big_operators.ring
import data.real.basic

@[ext] structure point := (x : ℝ) (y : ℝ) (z : ℝ)

namespace point

def add (a b : point) : point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

protected theorem add_assoc (a b c : point) :
  (a.add b).add c = a.add (b.add c) :=
by { simp [add, add_assoc] }

def smul (r : ℝ) (a : point) : point :=
⟨r * a.x, r * a.y, r * a.z⟩

theorem smul_distrib (r : ℝ) (a b : point) :
  (smul r a).add (smul r b) = smul r (a.add b) :=
by { simp [add, smul, mul_add] }

end point

structure standard_two_simplex :=
(x : ℝ)
(y : ℝ)
(z : ℝ)
(x_nonneg : 0 ≤ x)
(y_nonneg : 0 ≤ y)
(z_nonneg : 0 ≤ z)
(sum_eq   : x + y + z = 1)

namespace standard_two_simplex

noncomputable theory

def weighted_average (lambda : real)
    (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : standard_two_simplex) :
  standard_two_simplex :=
{ x        := lambda * a.x + (1 - lambda) * b.x,
  y        := lambda * a.y + (1 - lambda) * b.y,
  z        := lambda * a.z + (1 - lambda) * b.z,
  x_nonneg := add_nonneg (mul_nonneg lambda_nonneg a.x_nonneg)
                (mul_nonneg (by linarith) b.x_nonneg),
  y_nonneg := add_nonneg (mul_nonneg lambda_nonneg a.y_nonneg)
                (mul_nonneg (by linarith) b.y_nonneg),
  z_nonneg := add_nonneg (mul_nonneg lambda_nonneg a.z_nonneg)
                (mul_nonneg (by linarith) b.z_nonneg),
  sum_eq   :=
    begin
      transitivity (a.x + a.y + a.z) * lambda + (b.x + b.y + b.z) * (1 - lambda),
      { ring },
      simp [a.sum_eq, b.sum_eq]
    end }

end standard_two_simplex

open_locale big_operators

structure standard_simplex (n : ℕ) :=
(v          : fin n → ℝ)
(nonneg     : ∀ i : fin n, 0 ≤ v i)
(sum_eq_one : ∑ i, v i = 1)

namespace standard_simplex

def midpoint (n : ℕ) (a b : standard_simplex n) : standard_simplex n :=
{ v := λ i, (a.v i + b.v i) / 2,
  nonneg :=
    begin
      intro i,
      apply div_nonneg,
      { linarith [a.nonneg i, b.nonneg i] },
      norm_num
    end,
  sum_eq_one :=
    begin
      simp [div_eq_mul_inv, ←finset.sum_mul, finset.sum_add_distrib,
        a.sum_eq_one, b.sum_eq_one],
      field_simp
    end  }

end standard_simplex

namespace standard_simplex

def weighted_average {n : ℕ} (lambda : real)
    (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : standard_simplex n) : standard_simplex n :=
{ v          := λ i, lambda * a.v i + (1 - lambda) * b.v i,
  nonneg     := λ i, add_nonneg (mul_nonneg lambda_nonneg (a.nonneg i))
                  (mul_nonneg (by linarith) (b.nonneg i)),
  sum_eq_one :=
    begin
      transitivity lambda * (∑ i, a.v i) + (1 - lambda) * (∑ i, b.v i),
      { rw [finset.sum_add_distrib, finset.mul_sum, finset.mul_sum] },
      simp [a.sum_eq_one, b.sum_eq_one]
    end }

end standard_simplex