Set of Discontinuities of Baire Function is Meager

== Theorem ==
Let $X \subseteq \R$. 
Let $f : X \to \R$ be a Baire function.
Let $D$ be the set of points for which $f$ is discontinuous.
Let $d$ be the Euclidean metric on $\R$. 
Then $D$ is meager in the metric space $\struct {X, d}$.
== Proof ==
Since $f$ is a Baire function, there exists a sequence $\sequence {f_n}$ of continuous functions such that:
:$\sequence {f_n}$ converges pointwise to $f$.
For each $\epsilon > 0$, define:
:$\map F \epsilon = \set {x \in X : \map {\omega_f} x > \epsilon}$
where $\map {\omega_f} x$ denotes the oscillation of $f$ at $x$.
From Real Function is Continuous at Point iff Oscillation is Zero:
:$f$ is discontinuous at $x$ $\map {\omega_f} x > 0$.
Therefore:
:$\ds D = \bigcup_{i \mathop = 1}^\infty \map F {\frac 1 n}$
We aim to show that $\map F \epsilon$ is nowhere dense in $\struct {X, d}$ for each $\epsilon > 0$.
Let $I$ be an interval. 
We aim to show that there exists a subinterval $J$ of $I$ that is disjoint from $\map F \epsilon$.
From this, it will follow that $\map F \epsilon$ is nowhere dense from Open Ball Characterization of Denseness.
For each natural number $n$, let:
We can show that each $E_n$ is closed.
For each natural number $i, j$ define $g_{i, j} : X \to \R$ to have: 
:$\map {g_{i, j} } x = \size {\map {f_i} x - \map {f_j} x}$
From:
:Combined Sum Rule for Continuous Real Functions
:Absolute Value of Continuous Real Function is Continuous
We have:
:$g_{i, j}$ is continuous for each $i, j$. 
From Continuity Defined from Closed Sets, we have: 
:$\map {g^{-1}_{i, j} } {\closedint 0 {\dfrac \epsilon 4} }$ is closed for each $i, j$. 
Note that we can write:
:$\ds E_n = \bigcap_{i \mathop = n}^\infty \bigcap_{j \mathop = n}^\infty \map {g^{-1}_{i, j} } {\closedint 0 {\dfrac \epsilon 4} }$
This is an intersection of closed sets, so is itself closed by Intersection of Closed Sets is Closed.
Let:
:$\ds E = \bigcup_{i \mathop = 1}^\infty E_n$
Clearly:
:$E \subseteq I$
Since $\sequence {f_n}$ converges pointwise, the sequence $\sequence {\map {f_n} x}$ is Cauchy, from Convergent Sequence is Cauchy Sequence.
So, for each $x \in I$ there exists an $N$ such that: 
:$\size {\map {f_i} x - \map {f_j} x} \le \dfrac \epsilon 4$
for all $i, j \ge N$. 
That is:
:$x \in E_N \subseteq E$
So:
:$I \subseteq E$
giving:
:$E = I$
From Real Interval is Non-Meager:
:$I$ is not meager in the metric space $\struct {X, d}$.
So:
:at least one $E_n$ is not nowhere dense in $\struct {X, d}$.
Fix this $n$. 
Since $E_n$ is not nowhere dense, there exists some $J \subseteq E_n$ such that:
:$E_n \cap J$ is dense in $J$.
That is: 
:$\paren {E_n \cap J}^- = J$
From Closure of Intersection is Subset of Intersection of Closures, we have: 
:$\paren {E_n \cap J}^- \subseteq E_n^- \cap J^-$
From Set is Closed iff Equals Topological Closure:
:$E_n^- = E_n$
so, we have:
:$J \subseteq E_n \cap J^-$
We can therefore see that:
:$J \subseteq E_n$
We therefore have, for $x \in J$: 
:$\size {\map {f_i} x - \map {f_j} x} \le \dfrac \epsilon 4$
for all $i, j \ge n$. 
Taking $j = n$ and $i \to \infty$, we obtain:
:$\size {\map f x - \map {f_n} x} \le \dfrac \epsilon 4$
We now look at the difference:
:$\size {\map f y - \map f z}$
We have, by the Triangle Inequality:
:$\size {\map f y - \map f z} \le \size {\map f y - \map {f_n} y} + \size {\map {f_n} y - \map {f_n} z} + \size {\map {f_n} z - \map f z}$
Since each $f_n$ is continuous on $X$:
:$f_n$ is uniformly continuous on compact subsets of $X$
by Continuous Function on Compact Space is Uniformly Continuous.
So, there exists a closed interval $K \subseteq J$ such that: 
:$\size {\map {f_n} z - \map {f_n} y} \le \dfrac \epsilon 4$
for all $y, z \in K$. 
That is:
:$\size {\map f y - \map f z} \le \dfrac {3 \epsilon} 4$
for all $y, z \in K$.
So, for any $t \in K$, we have:
:$\map {\omega_f} t \le \dfrac {3 \epsilon} 4$
So, $K$ is disjoint from $\map F \epsilon$.
So each $\map F \epsilon$ is nowhere dense in $\struct {X, d}$.
Since $D$ is the countable union of nowhere dense sets in $\struct {X, d}$, it is meager in $\struct {X, d}$.
Category:Meager Spaces