Skip to content

fix: scope Exercise 1.2.2's boundedness hypothesis to its own conjunct - #650

Open
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:fix/ex-1-2-2-bound-scoping
Open

fix: scope Exercise 1.2.2's boundedness hypothesis to its own conjunct#650
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:fix/ex-1-2-2-bound-scoping

Conversation

@Chessing234

Copy link
Copy Markdown
Contributor

Exercise 1.2.2 currently reads

example : ∃ f: ℕ → ℝ → ℝ, ∃ F: ℝ → ℝ, ∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M ∧
    (∀ x ∈ Set.Icc 0 1, Filter.atTop.Tendsto (fun n ↦ f n x) (nhds (F x))) ∧
    (∀ n, RiemannIntegrableOn (f n) (Icc 0 1)) ∧
    ¬ RiemannIntegrableOn F (Icc 0 1) := by

binds tighter than the preceding binders, so ∀ n, ∀ x ∈ Icc 0 1 scopes over
the entire four-way conjunction rather than over |f n x| ≤ M alone. The three
later conjuncts mention neither n nor that x — the second rebinds its own
x, the third rebinds its own n, shadowing the outer one — so each is
re-asserted once per (n, x) pair.

Since and Icc 0 1 are both nonempty this is equivalent to the intended
statement, so nothing becomes provable or unprovable here. The cost is only that
a reader has to notice that equivalence before they can see what the exercise is
asking, and the shadowed ∀ n invites a misreading of the third conjunct.

The fix parenthesises the boundedness hypothesis as its own conjunct, which is
how Exercise 1.2.2' immediately below already writes exactly the same hypothesis:

(∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M) → ...

so the two neighbouring statements now agree on the shape of the shared
hypothesis.

Independent of #649, which touches Exercise 1.2.2' a few lines below; the changed
lines are disjoint, so the two merge in either order.

No Lean toolchain build was run for this — relying on the build CI on this PR.

The statement read

  ∃ M, ∀ n, ∀ x ∈ Set.Icc 0 1, |f n x| ≤ M ∧
    (pointwise convergence) ∧ (each fₙ Riemann integrable) ∧ (F not)

so `∀ n, ∀ x ∈ Icc 0 1` binds the whole conjunction, not just the
bound `|f n x| ≤ M`. The three later conjuncts mention neither `n` nor
that `x`, so each is re-asserted once per pair -- and the `∀ n` is
shadowed by the `∀ n` inside the third conjunct.

Modulo `ℕ` and `Icc 0 1` being nonempty this is equivalent to the
intended statement, so nothing is proved or unproved by the change; it
just stops the reader having to check that equivalence to see what the
exercise asks.

Parenthesise the bound as its own conjunct, matching how Exercise 1.2.2'
directly below already writes the same hypothesis.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant