theorem helperForTheorem_4_7_9_sin_shift_half_firstPositiveSineZero_eq_cos (x : ℝ) : Real.sin (x + firstPositiveSineZero / 2) = Real.cos x

Helper for Theorem 4.7.9: shifting by firstPositiveSineZero / 2 converts Real.sin to Real.cos.

theorem helperForTheorem_4_7_9_shifted_division_formula (x : ℝ) : (x + firstPositiveSineZero / 2) / firstPositiveSineZero = x / firstPositiveSineZero + 1 / 2

Helper for Theorem 4.7.9: division by firstPositiveSineZero after the half-period shift simplifies to adding 1/2.

theorem helperForTheorem_4_7_9_exists_integer_shifted_iff_half_integer (x : ℝ) : (∃ (n : ℤ), (x + firstPositiveSineZero / 2) / firstPositiveSineZero = ↑n) ↔ ∃ (n : ℤ), x / firstPositiveSineZero = ↑n + 1 / 2

Helper for Theorem 4.7.9: integer-valuedness of the shifted quotient is equivalent to half-integer-valuedness of the original quotient.

theorem helperForTheorem_4_7_9_cos_zero_iff_shifted_sin_zero (x : ℝ) : Real.cos x = 0 ↔ Real.sin (x + firstPositiveSineZero / 2) = 0

Helper for Theorem 4.7.9: Real.cos x = 0 is equivalent to vanishing of the shifted sine value.

theorem real_cos_eq_zero_iff_div_firstPositiveSineZero_half_integer (x : ℝ) : Real.cos x = 0 ↔ ∃ (n : ℤ), x / firstPositiveSineZero = ↑n + 1 / 2

Theorem 4.7.9: For every real number x (with π given by Definition 4.7.2), Real.cos x = 0 if and only if x / π is an integer plus (1/2).

theorem helperForProposition_4_7_11_hasSum_alternating_inv_odd_pi_div_four_conditional : HasSum (fun (n : ℕ) => (-1) ^ n / (2 * ↑n + 1)) (Real.pi / 4) (SummationFilter.conditional ℕ)

Helper for Proposition 4.7.11: the Leibniz series gives π / 4 for the conditional summation filter on ℕ.

theorem helperForProposition_4_7_11_firstPositiveSineZero_eq_four_mul_conditional_tsum : firstPositiveSineZero = 4 * ∑'[SummationFilter.conditional ℕ] (n : ℕ), (-1) ^ n / (2 * ↑n + 1)

Helper for Proposition 4.7.11: the conditionally summed Leibniz identity for firstPositiveSineZero (hence for π).

theorem helperForProposition_4_7_11_not_summable_inv_odd : ¬Summable fun (n : ℕ) => 1 / (2 * ↑n + 1)

Helper for Proposition 4.7.11: the odd reciprocal series is not unconditionally summable.

theorem helperForProposition_4_7_11_not_summable_alternating_inv_odd : ¬Summable fun (n : ℕ) => (-1) ^ n / (2 * ↑n + 1)

Helper for Proposition 4.7.11: the alternating odd-reciprocal series is not unconditionally summable.

theorem helperForProposition_4_7_11_tsum_alternating_inv_odd_eq_zero : ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) = 0

Helper for Proposition 4.7.11: under Lean's default unconditional tsum, the alternating odd-reciprocal series has value 0.

theorem helperForProposition_4_7_11_four_mul_tsum_alternating_inv_odd_eq_zero : 4 * ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) = 0

Helper for Proposition 4.7.11: consequently, 4 * ∑' n, (-1)^n / (2n+1) is 0 under unconditional tsum.

theorem helperForProposition_4_7_11_eq_four_mul_tsum_implies_firstPositiveSineZero_eq_zero (hmain : firstPositiveSineZero = 4 * ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1)) : firstPositiveSineZero = 0

Helper for Proposition 4.7.11: the unconditional-series equality would force firstPositiveSineZero = 0.

theorem helperForProposition_4_7_11_lower_bound : 4 - 4 / 3 < firstPositiveSineZero

Helper for Proposition 4.7.11: lower bound 4 - 4/3 < firstPositiveSineZero.

theorem helperForProposition_4_7_11_upper_bound : firstPositiveSineZero < 4

Helper for Proposition 4.7.11: upper bound firstPositiveSineZero < 4.

theorem helperForProposition_4_7_11_bounds_conjunction : 4 - 4 / 3 < firstPositiveSineZero ∧ firstPositiveSineZero < 4

Helper for Proposition 4.7.11: package the two stated numerical bounds into a single conjunction.

theorem helperForProposition_4_7_11_not_firstPositiveSineZero_eq_four_mul_tsum_alternating_inv_odd : ¬firstPositiveSineZero = 4 * ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1)

Helper for Proposition 4.7.11: under unconditional tsum, the asserted Leibniz equality would force firstPositiveSineZero = 0, contradicting firstPositiveSineZero = Real.pi.

theorem helperForProposition_4_7_11_not_target_conjunction : ¬(firstPositiveSineZero = 4 * ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) ∧ 4 - 4 / 3 < firstPositiveSineZero ∧ firstPositiveSineZero < 4)

Helper for Proposition 4.7.11: the full conjunction in the target statement is inconsistent with unconditional tsum for this series.

theorem helperForProposition_4_7_11_false_of_main_conjunct_and_bounds (hmain : firstPositiveSineZero = 4 * ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1)) (hbounds : 4 - 4 / 3 < firstPositiveSineZero ∧ firstPositiveSineZero < 4) : False

Helper for Proposition 4.7.11: combining any witness of the main Leibniz equality with the proven numerical bounds yields a contradiction under unconditional tsum.

theorem firstPositiveSineZero_eq_four_mul_tsum_alternating_inv_odd_and_bounds : firstPositiveSineZero = 4 * ∑'[SummationFilter.conditional ℕ] (n : ℕ), (-1) ^ n / (2 * ↑n + 1) ∧ 4 - 4 / 3 < firstPositiveSineZero ∧ firstPositiveSineZero < 4

Proposition 4.7.11: the Leibniz series identity π = 4 * (1 - 1/3 + 1/5 - 1/7 + ⋯) holds in Lean via the conditional summation filter on ℕ; in particular, 4 - 4/3 < π < 4.

theorem helperForProposition_4_7_12_termContinuous (n : ℕ) : Continuous fun (x : ℝ) => 1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)

Helper for Proposition 4.7.12: each summand in the scaled cosine series is continuous.

theorem helperForProposition_4_7_12_majorantSummable : Summable fun (n : ℕ) => 1 / 4 ^ (n + 1)

Helper for Proposition 4.7.12: the geometric majorant 4^{-(n+1)} is summable.

theorem helperForProposition_4_7_12_termNormBound (n : ℕ) (x : ℝ) : ‖1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)‖ ≤ 1 / 4 ^ (n + 1)

Helper for Proposition 4.7.12: each summand is bounded in norm by 4^{-(n+1)}.

theorem helperForProposition_4_7_12_uniformLimit_raw : TendstoUniformly (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, 1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)) scaledCosineSeriesFunction Filter.atTop

Helper for Proposition 4.7.12: partial sums converge uniformly to the infinite series.

theorem helperForProposition_4_7_12_partialSumsContinuous (N : ℕ) : Continuous fun (x : ℝ) => ∑ n ∈ Finset.range N, 1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)

Helper for Proposition 4.7.12: each partial sum in the scaled cosine series is continuous.

theorem scaledCosineSeries_uniformly_convergent_and_continuous : TendstoUniformly (fun (N : ℕ) (x : ℝ) => ∑ n ∈ Finset.range N, 1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)) scaledCosineSeriesFunction Filter.atTop ∧ Continuous scaledCosineSeriesFunction

Proposition 4.7.12: for f(x) = ∑_{n=1}^∞ 4^{-n} cos(32^n π x) (with π = firstPositiveSineZero from Definition 4.7.2), the series converges uniformly on ℝ; in particular, f is continuous on ℝ.

noncomputable def helperForProposition_4_7_13_diffTerm (j : ℤ) (m n : ℕ) : ℝ

Helper for Proposition 4.7.13: the n-th increment term of scaledCosineSeriesFunction across mesh size 32^{-m}.

Equations

• One or more equations did not get rendered due to their size.

theorem helperForProposition_4_7_13_seriesSummableAtPoint (x : ℝ) : Summable fun (n : ℕ) => 1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)

Helper for Proposition 4.7.13: pointwise summability of the cosine series.

theorem helperForProposition_4_7_13_phaseShift_asTwoPiMultiple (m n : ℕ) (hmn : m ≤ n) : ∃ (k : ℕ), 32 ^ (n + 1 - m) * firstPositiveSineZero = ↑k * (2 * Real.pi)

Helper for Proposition 4.7.13: for n ≥ m, the phase shift 32^(n+1-m) * π is an integer multiple of 2π.

theorem helperForProposition_4_7_13_highModesVanish (j : ℤ) (m n : ℕ) (hnm : m ≤ n) : helperForProposition_4_7_13_diffTerm j m n = 0

Helper for Proposition 4.7.13: all modes n ≥ m vanish in the increment.

theorem helperForProposition_4_7_13_increment_asFiniteSum (j : ℤ) (m : ℕ) : scaledCosineSeriesFunction (↑(j + 1) / 32 ^ m) - scaledCosineSeriesFunction (↑j / 32 ^ m) = ∑ n ∈ Finset.range m, helperForProposition_4_7_13_diffTerm j m n

Helper for Proposition 4.7.13: the increment equals a finite sum over modes < m.

theorem helperForProposition_4_7_13_mainMode_exact (j : ℤ) (m : ℕ) (hm : 1 ≤ m) : |helperForProposition_4_7_13_diffTerm j m (m - 1)| = 2 / 4 ^ m

Helper for Proposition 4.7.13: the main mode n = m-1 contributes exactly 2 / 4^m in absolute value.

theorem helperForProposition_4_7_13_sumPowEight_bound (m : ℕ) (hm : 1 ≤ m) : ∑ n ∈ Finset.range (m - 1), 8 ^ (n + 1) ≤ 8 ^ m / 7

Helper for Proposition 4.7.13: finite geometric bound for ∑_{n < m-1} 8^{n+1}.

theorem helperForProposition_4_7_13_singleLowMode_absBound (j : ℤ) (m n : ℕ) : |helperForProposition_4_7_13_diffTerm j m n| ≤ Real.pi / 32 ^ m * 8 ^ (n + 1)

Helper for Proposition 4.7.13: each increment mode is bounded by a Lipschitz estimate for cosine.

theorem helperForProposition_4_7_13_lowMode_sumAbs_bound (j : ℤ) (m : ℕ) : ∑ n ∈ Finset.range (m - 1), |helperForProposition_4_7_13_diffTerm j m n| ≤ Real.pi / 32 ^ m * ∑ n ∈ Finset.range (m - 1), 8 ^ (n + 1)

Helper for Proposition 4.7.13: the finite sum of absolute low-mode terms is bounded by the corresponding geometric series.

theorem helperForProposition_4_7_13_lowMode_series_to_quarterPow (m : ℕ) (hm : 1 ≤ m) : Real.pi / 32 ^ m * (8 ^ m / 7) ≤ 1 / 4 ^ m

Helper for Proposition 4.7.13: the geometric-factor estimate implies the final 1 / 4^m bound.

theorem helperForProposition_4_7_13_lowModes_bound (j : ℤ) (m : ℕ) (hm : 1 ≤ m) : |∑ n ∈ Finset.range (m - 1), helperForProposition_4_7_13_diffTerm j m n| ≤ 1 / 4 ^ m

Helper for Proposition 4.7.13: the sum of low modes n < m-1 is bounded by 1 / 4^m in absolute value.

theorem helperForProposition_4_7_13_absLowerBound_from_main_plus_error (m : ℕ) {main error : ℝ} (hmain : |main| = 2 / 4 ^ m) (herror : |error| ≤ 1 / 4 ^ m) : |main + error| ≥ 1 / 4 ^ m

Helper for Proposition 4.7.13: if the main term has size 2/4^m and the error is bounded by 1/4^m, then the total has size at least 1/4^m.

theorem scaledCosineSeries_increment_lower_bound (j : ℤ) (m : ℕ) (hm : 1 ≤ m) : |scaledCosineSeriesFunction (↑(j + 1) / 32 ^ m) - scaledCosineSeriesFunction (↑j / 32 ^ m)| ≥ 1 / 4 ^ m

Proposition 4.7.13: for every j : ℤ and every integer m ≥ 1, for f(x) = ∑_{n=1}^∞ 4^{-n} cos(32^n π x) (with π = firstPositiveSineZero), the increment across consecutive points of mesh size 32^{-m} satisfies |f((j+1)/32^m) - f(j/32^m)| ≥ 4^{-m}.