Truncated sine-square function

PDF p. 13: Definition before Lemma 2.3; PDF p. 14: Figure 1

For a real angle $\theta \in (-\pi ,\pi ]$, let $\mathrm{\mid }\theta \mathrm{\mid }$ denote its absolute value, and let $\sin$ be the real sine function. Define $H:(-\pi ,\pi ]\to \mathbb{R}$ by $H(\theta )={\sin }^2(\mathrm{\mid }\theta \mathrm{\mid })$ when $\mathrm{\mid }\theta \mathrm{\mid }\le \pi \mathrm{/}2$, and $H(\theta )=1$ when $\pi \mathrm{/}2\le \mathrm{\mid }\theta \mathrm{\mid }\le \pi$. The two formulas agree where their conditions overlap. Figure 1 of the article plots this function.

Absolute value in an ordered field

Real sine as the restriction of complex sine

Given: A real $\theta \in (-\pi ,\pi ]$.

Goal: Show that the displayed rule assigns exactly one real value to $H(\theta )$.

1.1 By [F4], $\pi >0$. By [F3], if $\theta \ge 0$ then $\mathrm{\mid }\theta \mathrm{\mid }=\theta \in [0,\pi ]$; if $\theta <0$ then $\mathrm{\mid }\theta \mathrm{\mid }=-\theta \in (0,\pi )$, since $-\pi <\theta <0$. Thus $0\le \mathrm{\mid }\theta \mathrm{\mid }\le \pi$, so at least one branch applies, and both apply only when $\mathrm{\mid }\theta \mathrm{\mid }=\pi \mathrm{/}2$. The sine branch is a real value by [F1], and the other branch is the real number $1$. [F1, F3, F4, given, algebra]

2.1 At the overlap, [F2] gives ${\sin }^2(\mathrm{\mid }\theta \mathrm{\mid })={\sin }^2(\pi \mathrm{/}2)=1$, equal to the second branch. Consequently the rule defines one real value for every point of the stated domain. [F2, step 1.1, algebra] ∎

The definition and its plotted domain are attributed to the article, PDF pp. 13–14, immediately before Lemma 2.3 and in Figure 1.