About the Typesetting of Mathematics in Lean C06S01

Stream: general

[Zhu]

In the later part of section 6.1. Defining structures, it appears that a subsection has been mistakenly typeset together with the previous subsection due to the latter ending with a separate SOLUTIONS-/ without /-EXAMPLES

I tried adding a blank line before SOLUTIONS: -/, and it resolved the problem.

prt.png

[Zhu]

here's the original source code

/- TEXT:
As an exercise, see if you can define the weighted average of
two points in the standard :math:`n`-simplex.
You can use ``Finset.sum_add_distrib``
and ``Finset.mul_sum`` to manipulate the relevant sums.
SOLUTIONS: -/
namespace StandardSimplex

def weightedAverage {n : ℕ} (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardSimplex n) : StandardSimplex n
    where
  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 := by
    trans (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 StandardSimplex

/- TEXT:
We have seen that structures can be used to bundle together data
and properties.
Interestingly, they can also be used to bundle together properties
without the data.
For example, the next structure, ``IsLinear``, bundles together
the two components of linearity.

[Patrick Massot]

Thanks for this report.