theorem helperForTheorem_8_3_not_diophantineExponent_of_rat {τ : ℝ} (p : ℤ) (q : ℕ) (hq : 0 < q) : ¬helperForTheorem_8_3_diophantineExponent τ (↑p / ↑q)

Helper for Theorem 8.3: every rational number fails a fixed-exponent Diophantine lower bound with a strictly positive constant.

theorem helperForTheorem_8_3_rat_mem_complement {τ : ℝ} (r : ℚ) : ↑r ∈ {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}

Helper for Theorem 8.3: every rational number lies in the complement of the fixed-exponent Diophantine set.

theorem helperForTheorem_8_3_range_rat_subset_complement {τ : ℝ} : Set.range Rat.cast ⊆ {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}

Helper for Theorem 8.3: the embedded rationals form a subset of the fixed-exponent complement.

theorem helperForTheorem_8_3_int_mem_complement {τ : ℝ} (p : ℤ) : ↑p ∈ {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}

Helper for Theorem 8.3: every integer belongs to the complement of the fixed-exponent Diophantine set.

theorem helperForTheorem_8_3_complement_nonempty {τ : ℝ} : {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}.Nonempty

Helper for Theorem 8.3: the complement of the fixed-exponent Diophantine set is nonempty (for instance, it contains rational numbers).

theorem helperForTheorem_8_3_complement_infinite {τ : ℝ} : {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}.Infinite

Helper for Theorem 8.3: the complement of the fixed-exponent Diophantine set is infinite because it contains every integer.

theorem helperForTheorem_8_3_not_diophantineExponent_iff_forall_pos_constant_exists_close_rational {τ x : ℝ} : ¬helperForTheorem_8_3_diophantineExponent τ x ↔ ∀ (c : ℝ), 0 < c → ∃ (p : ℤ) (q : ℕ), 0 < q ∧ |x - ↑p / ↑q| < c / ↑q ^ τ

Helper for Theorem 8.3: negating the fixed-exponent Diophantine lower-bound is equivalent to saying that every positive constant is violated by some rational approximation.

theorem helperForTheorem_8_3_complement_antitone_in_exponent {τ τ' : ℝ} (hττ' : τ ≤ τ') : {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ' x} ⊆ {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}

Helper for Theorem 8.3: if τ ≤ τ', then the complement of the τ'-Diophantine set is contained in the complement of the τ-Diophantine set.

theorem helperForTheorem_8_3_volume_complement_antitone_in_exponent {τ τ' : ℝ} (hττ' : τ ≤ τ') : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ' x} ≤ MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x}

Helper for Theorem 8.3: the complement-measure is antitone with respect to the Diophantine exponent.

theorem helperForTheorem_8_3_ae_isDiophantineReal_of_ae_diophantineExponent_gt_one {τ : ℝ} (hτ : 1 < τ) (hae : ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: if a fixed exponent τ > 1 Diophantine lower bound holds Lebesgue-almost everywhere, then IsDiophantineReal also holds almost everywhere.

theorem helperForTheorem_8_3_volume_not_isDiophantineReal_zero_of_ae_diophantineExponent_gt_one {τ : ℝ} (hτ : 1 < τ) (hae : ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: an almost-everywhere fixed-exponent bound with τ > 1 forces the complement of IsDiophantineReal to have Lebesgue measure zero.

theorem helperForTheorem_8_3_ae_isDiophantineReal_of_full_measure_pair {τ : ℝ} (hτ : 1 < τ) (hpair : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: a full-measure fixed-exponent Diophantine pair with τ > 1 implies that IsDiophantineReal holds almost everywhere.

theorem helperForTheorem_8_3_volume_not_isDiophantineReal_zero_of_full_measure_pair {τ : ℝ} (hτ : 1 < τ) (hpair : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: a full-measure fixed-exponent Diophantine pair with τ > 1 forces the non-diophantine set to have measure zero.

theorem helperForTheorem_8_3_zero_not_diophantineExponent_two : ¬helperForTheorem_8_3_diophantineExponent 2 0

Helper for Theorem 8.3: at exponent τ = 2, the origin fails the fixed-exponent Diophantine lower bound.

theorem helperForTheorem_8_3_int_mem_complement_two (p : ℤ) : ↑p ∈ {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent 2 x}

Helper for Theorem 8.3: at exponent τ = 2, every integer lies in the complement of the fixed-exponent Diophantine set.

theorem helperForTheorem_8_3_complement_nonempty_two : {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent 2 x}.Nonempty

Helper for Theorem 8.3: at exponent τ = 2, the complement of the fixed-exponent Diophantine set is nonempty.

theorem helperForTheorem_8_3_ae_isDiophantineReal_of_full_measure_pair_two (hpair : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent 2 x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent 2 x) : ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: a full-measure fixed-exponent pair at τ = 2 implies IsDiophantineReal almost everywhere.

theorem helperForTheorem_8_3_volume_not_isDiophantineReal_zero_of_full_measure_pair_two (hpair : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent 2 x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent 2 x) : MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: a full-measure fixed-exponent pair at τ = 2 forces the non-diophantine set to have Lebesgue measure zero.

theorem helperForTheorem_8_3_consequences_of_full_measure_pair_two (hpair : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent 2 x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent 2 x) : (∀ᵐ (x : ℝ), IsDiophantineReal x) ∧ MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: at τ = 2, a full-measure fixed-exponent pair yields both almost-everywhere IsDiophantineReal and measure-zero non-diophantine complement.

theorem helperForTheorem_8_3_full_measure_pair_two_of_universal_fixed_exponent_claim (hall : ∀ (τ : ℝ), 1 < τ → MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent 2 x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent 2 x

Helper for Theorem 8.3: any universal fixed-exponent full-measure claim for all τ > 1 specializes to the case τ = 2.

theorem helperForTheorem_8_3_ae_isDiophantineReal_of_universal_fixed_exponent_claim (hall : ∀ (τ : ℝ), 1 < τ → MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: a universal fixed-exponent full-measure claim would imply IsDiophantineReal almost everywhere by specializing to τ = 2.

theorem helperForTheorem_8_3_volume_not_isDiophantineReal_zero_of_universal_fixed_exponent_claim (hall : ∀ (τ : ℝ), 1 < τ → MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: a universal fixed-exponent full-measure claim would force the non-diophantine set to have Lebesgue measure zero.

theorem helperForTheorem_8_3_consequences_of_universal_fixed_exponent_claim (hall : ∀ (τ : ℝ), 1 < τ → MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : (∀ᵐ (x : ℝ), IsDiophantineReal x) ∧ MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: a universal fixed-exponent full-measure claim yields both almost-everywhere IsDiophantineReal and measure-zero non-diophantine complement.

theorem helperForTheorem_8_3_ae_consequences_of_volume_complement_zero {τ : ℝ} (hτ : 1 < τ) (hnull : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0) : (∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ∧ ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: once the fixed-exponent complement has measure zero, one gets both the almost-everywhere exponent-τ bound and almost-everywhere IsDiophantineReal (for τ > 1).

theorem helperForTheorem_8_3_full_measure_pair_of_hτ_and_volume_complement_zero {τ : ℝ} (hτ : 1 < τ) (hnull : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0) : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x

Helper for Theorem 8.3: for a fixed exponent τ > 1, the theorem's target full-measure pair follows from the null-complement statement.

theorem helperForTheorem_8_3_full_measure_pair_iff_volume_complement_zero_of_gt_one {τ : ℝ} (hτ : 1 < τ) : (MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ↔ MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0

Helper for Theorem 8.3: for a fixed exponent τ > 1, proving the theorem's target pair is equivalent to proving the null-complement statement.

theorem helperForTheorem_8_3_target_pair_and_ae_isDiophantineReal_of_hτ_and_volume_complement_zero {τ : ℝ} (hτ : 1 < τ) (hnull : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0) : (MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ∧ ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: from a fixed exponent τ > 1 null-complement statement, one obtains both the theorem's target full-measure pair and almost-everywhere IsDiophantineReal.

theorem helperForTheorem_8_3_target_pair_iff_target_pair_and_ae_isDiophantineReal {τ : ℝ} (hτ : 1 < τ) : (MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ↔ (MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) ∧ ∀ᵐ (x : ℝ), IsDiophantineReal x

Helper for Theorem 8.3: for τ > 1, augmenting the theorem's target pair with the derived almost-everywhere IsDiophantineReal consequence is equivalent to the target pair itself.

theorem helperForTheorem_8_3_consequences_of_target_pair {τ : ℝ} (hτ : 1 < τ) (hpair : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x) : (∀ᵐ (x : ℝ), IsDiophantineReal x) ∧ MeasureTheory.volume {x : ℝ | ¬IsDiophantineReal x} = 0

Helper for Theorem 8.3: for a fixed exponent τ > 1, the theorem's target pair implies both almost-everywhere IsDiophantineReal and measure-zero non-IsDiophantineReal complement.

theorem helperForTheorem_8_3_positive_lower_bound_for_bounded_denominators_nonrat {τ x : ℝ} (hτ : 0 ≤ τ) (hx_nonrat : x ∉ Set.range Rat.cast) (N : ℕ) : ∃ (c : ℝ), 0 < c ∧ ∀ (p : ℤ) (q : ℕ), 0 < q → q ≤ N → c / ↑q ^ τ ≤ |x - ↑p / ↑q|

Helper for Theorem 8.3: a nonrational real has a uniform positive lower bound for |x - p/q| against all integers p and all positive denominators q ≤ N; with τ ≥ 0, this yields a bound of the form c / q^τ.

theorem helperForTheorem_8_3_liouvilleWith_of_not_diophantineExponent_nonrat {τ x : ℝ} (hτ : 0 ≤ τ) (hx_nonrat : x ∉ Set.range Rat.cast) (hnot : ¬helperForTheorem_8_3_diophantineExponent τ x) : LiouvilleWith τ x

Helper for Theorem 8.3: for nonrational x and nonnegative exponent τ, failure of the fixed-exponent Diophantine lower bound implies LiouvilleWith τ x.

theorem helperForTheorem_8_3_complement_subset_rat_or_liouvilleWith {τ : ℝ} (hτ : 0 ≤ τ) : {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} ⊆ Set.range Rat.cast ∪ {x : ℝ | LiouvilleWith τ x}

Helper for Theorem 8.3: the complement of the fixed-exponent Diophantine set is contained in the union of the embedded rationals and the fixed-exponent Liouville set (for nonnegative exponent).

theorem helperForTheorem_8_3_volume_complement_zero_of_gt_two {τ : ℝ} (hτ : 2 < τ) : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0

Helper for Theorem 8.3: for τ > 2, the complement of the fixed-exponent Diophantine set has Lebesgue measure zero.

theorem theorem_8_3_full_measure_diophantine_exponent {τ : ℝ} (hτ : 2 < τ) : MeasureTheory.volume {x : ℝ | ¬helperForTheorem_8_3_diophantineExponent τ x} = 0 ∧ ∀ᵐ (x : ℝ), helperForTheorem_8_3_diophantineExponent τ x

Theorem 8.3: if τ > 2, then the set of real numbers x for which there exists c(x) > 0 such that |x - p/q| ≥ c(x) / q^τ for all p ∈ ℤ and q ∈ ℕ with q > 0 has full Lebesgue measure; equivalently, this Diophantine bound holds for Lebesgue-almost every real x.

theorem helperForProposition_8_7_geometric_series_ne_top : ∑' (n : ℕ), (1 / 2) ^ (n + 1) ≠ ⊤

Helper for Proposition 8.7: the shifted geometric series with ratio 1/2 is finite in ℝ≥0∞.

theorem helperForProposition_8_7_superlevel_measure_bound (f : ℕ → ℝ → ℝ) (hmeas : ∀ (n : ℕ), AEMeasurable (f n) MeasureTheory.volume) (hintegral : ∀ (n : ℕ), 1 ≤ n → ∫⁻ (x : ℝ), ENNReal.ofReal (f n x) ≤ (1 / 4) ^ n) (n : ℕ) : MeasureTheory.volume {x : ℝ | (1 / 2) ^ (n + 1) ≤ ENNReal.ofReal (f (n + 1) x)} ≤ (1 / 2) ^ (n + 1)

Helper for Proposition 8.7: Markov/Chebyshev gives the superlevel-set measure bound m({x | 2^{-(n+1)} ≤ f_{n+1}(x)}) ≤ 2^{-(n+1)}.

theorem helperForProposition_8_7_volume_limsup_zero (A : ℕ → Set ℝ) (hA : ∀ (n : ℕ), MeasureTheory.volume (A n) ≤ (1 / 2) ^ (n + 1)) : MeasureTheory.volume (Filter.limsup A Filter.atTop) = 0

Helper for Proposition 8.7: the limsup of superlevel sets has Lebesgue measure zero.

theorem helperForProposition_8_7_eventually_upper_bound_outside_limsup (f : ℕ → ℝ → ℝ) (hnonneg : ∀ (n : ℕ) (x : ℝ), 0 ≤ f n x) (x : ℝ) (hx : x ∉ Filter.limsup (fun (n : ℕ) => {y : ℝ | (1 / 2) ^ (n + 1) ≤ ENNReal.ofReal (f (n + 1) y)}) Filter.atTop) : ∀ᶠ (n : ℕ) in Filter.atTop, f (n + 1) x ≤ (1 / 2) ^ (n + 1)

Helper for Proposition 8.7: outside the limsup superlevel set, one eventually has the pointwise bound f_{n+1}(x) ≤ 2^{-(n+1)}.

theorem helperForProposition_8_7_tendsto_shifted_then_unshift (f : ℕ → ℝ → ℝ) (x : ℝ) (hnonneg : ∀ (n : ℕ) (y : ℝ), 0 ≤ f n y) (hbound : ∀ᶠ (n : ℕ) in Filter.atTop, f (n + 1) x ≤ (1 / 2) ^ (n + 1)) : Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds 0)

Helper for Proposition 8.7: an eventual geometric bound on the shifted sequence implies f_n(x) → 0.

theorem proposition_8_7_tendsto_zero_outside_small_exceptional_set (f : ℕ → ℝ → ℝ) (hmeas : ∀ (n : ℕ), AEMeasurable (f n) MeasureTheory.volume) (hnonneg : ∀ (n : ℕ) (x : ℝ), 0 ≤ f n x) (hintegral : ∀ (n : ℕ), 1 ≤ n → ∫⁻ (x : ℝ), ENNReal.ofReal (f n x) ≤ (1 / 4) ^ n) (ε : ℝ) : 0 < ε → ∃ (E : Set ℝ), MeasurableSet E ∧ MeasureTheory.volume E ≤ ENNReal.ofReal ε ∧ ∀ x ∈ Eᶜ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds 0)

Proposition 8.7: if (f_n)_{n ≥ 1} are nonnegative Lebesgue measurable functions on ℝ with ∫⁻ f_n dm ≤ 4^{-n} for all n ≥ 1, then for every ε > 0 there exists a Lebesgue measurable set E with m(E) ≤ ε such that f_n x → 0 for all x ∈ ℝ \ E.

theorem helperForTheorem_8_4_stronglyMeasurable_seq_on_Icc (f : ℕ → ↑(Set.Icc 0 1) → ℝ) (hmeas : ∀ (n : ℕ), Measurable (f n)) (n : ℕ) : MeasureTheory.StronglyMeasurable (f n)

Helper for Theorem 8.4: measurable functions on [0,1] are strongly measurable.

theorem helperForTheorem_8_4_ae_tendsto_zero_on_Icc (f : ℕ → ↑(Set.Icc 0 1) → ℝ) (hlim : ∀ (x : ↑(Set.Icc 0 1)), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds 0)) : ∀ᵐ (x : ↑(Set.Icc 0 1)), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds ((fun (x : ↑(Set.Icc 0 1)) => 0) x))

Helper for Theorem 8.4: pointwise convergence to zero implies almost-everywhere convergence to the zero function on [0,1].

theorem helperForTheorem_8_4_apply_mathlib_egorov_finite_measure (f : ℕ → ↑(Set.Icc 0 1) → ℝ) (hmeas : ∀ (n : ℕ), Measurable (f n)) (hlim : ∀ (x : ↑(Set.Icc 0 1)), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds 0)) {ε : ℝ} (hε : 0 < ε) : ∃ (E : Set ↑(Set.Icc 0 1)), MeasurableSet E ∧ MeasureTheory.volume E ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun (n : ℕ) => f n) (fun (x : ↑(Set.Icc 0 1)) => 0) Filter.atTop Eᶜ

Helper for Theorem 8.4: Egorov's theorem on the finite-measure space [0,1].

theorem theorem_8_4_egoroff_on_unit_interval (f : ℕ → ↑(Set.Icc 0 1) → ℝ) (hmeas : ∀ (n : ℕ), Measurable (f n)) (hnonneg : ∀ (n : ℕ) (x : ↑(Set.Icc 0 1)), 0 ≤ f n x) (hlim : ∀ (x : ↑(Set.Icc 0 1)), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds 0)) (ε : ℝ) : 0 < ε → ∃ (E : Set ↑(Set.Icc 0 1)), MeasurableSet E ∧ MeasureTheory.volume E ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun (n : ℕ) => f n) (fun (x : ↑(Set.Icc 0 1)) => 0) Filter.atTop Eᶜ

Theorem 8.4 (Egoroff on [0,1]): if (f_n) are measurable and nonnegative on [0,1] and satisfy f_n(x) → 0 for every x ∈ [0,1], then for every ε > 0 there exists a measurable E ⊆ [0,1] with m(E) ≤ ε such that f_n → 0 uniformly on [0,1] \ E.

theorem helperForProposition_8_8_shiftedDiagonal_term_eq_ite_eq (n m : ℕ) : ↑(if m + 1 = n + 1 then 1 else 0) = ↑(if m = n then 1 else 0)

Helper for Proposition 8.8: rewrite the shifted diagonal term into Kronecker-delta form.

theorem helperForProposition_8_8_row_hasSum_one (n : ℕ) : HasSum (fun (m : ℕ) => ↑(if m = n then 1 else 0)) 1

Helper for Proposition 8.8: each row of the diagonal indicator has sum 1.

theorem helperForProposition_8_8_column_tendsto_zero (m : ℕ) : Filter.Tendsto (fun (n : ℕ) => ↑(if n = m then 1 else 0)) Filter.atTop (nhds 0)

Helper for Proposition 8.8: each fixed column converges pointwise to 0.

theorem helperForProposition_8_8_rowSum_tendsto_one : Filter.Tendsto (fun (n : ℕ) => ∑' (m : ℕ), ↑(if m = n then 1 else 0)) Filter.atTop (nhds 1)

Helper for Proposition 8.8: the row sums converge to 1.

theorem helperForProposition_8_8_tsum_of_pointwise_limits_eq_zero : ∑' (x : ℕ), 0 = 0

Helper for Proposition 8.8: the sum of the pointwise limit function 0 is 0.

theorem proposition_8_8_exists_bounded_nonnegative_function_with_noncommuting_limit_and_series : ∃ (f : ℕ × ℕ → NNReal), (∃ (C : NNReal), ∀ (n m : ℕ), f (n, m) ≤ C) ∧ (∀ (n : ℕ), Summable fun (m : ℕ) => ↑(f (n, m + 1))) ∧ (∀ (m : ℕ), ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ↑(f (n, m + 1))) Filter.atTop (nhds l)) ∧ ∃ (g : ℕ → ℝ), (∀ (m : ℕ), Filter.Tendsto (fun (n : ℕ) => ↑(f (n, m + 1))) Filter.atTop (nhds (g m))) ∧ Summable g ∧ ∃ (L : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑' (m : ℕ), ↑(f (n, m + 1))) Filter.atTop (nhds L) ∧ L ≠ ∑' (m : ℕ), g m

Proposition 8.8: there exists a bounded function f : ℕ × ℕ → ℝ≥0 such that (i) for every n, the series ∑_{m=1}^∞ f(n,m) converges; (ii) for every m, the limit lim_{n→∞} f(n,m) exists; (iii) nevertheless, the limit of row sums is not equal to the sum of pointwise limits.