Remark 1.3.10: binary-to-ternary function implementation and helper construction #428
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Add Remark_1_3_10 namespace with BinaryToTernaryProperties structure - Add detailed proof sketch with domain/codomain considerations - Structure binary-to-ternary function construction and properties - Update example to use new namespace structure
- Explicitly use UnsignedMeasurable.TFAE to reduce to condition (viii)
- Apply List.TFAE.out to get equivalence: UnsignedMeasurable f ↔ ∀ t, LebesgueMeasurable {x | f x ≤ t}
- Reduce proof goal to showing sublevel sets are measurable
- Improve comments explaining the proof strategy using monotonicity
- Add zero_outside property to BinaryToTernaryProperties structure - Add helper lemmas: f_le_one, f_zero_outside, sublevel_set_measurable - Complete f_measurable cases: t < 0 (empty set), t ≥ 1 (universal set), structure for 0 < t < 1 - Enhance documentation for binaryToTernary_exists and exists_nonmeasurable_with_cantor_image - Improve proof sketches in main example preimage case
- Add zero_at_zero and zero_set_countable properties to BinaryToTernaryProperties
- Add f_zero_at_zero and f_zero_set_in_interval_countable helper lemmas
- Complete f_zero_set_measurable proof: decompose {f = 0} into open set and countable set
- Remove unused and incorrect lemmas: f_zero_set_eq, iic_union_ioi_measurable
- Fix comment: dyadic rationals = terminating binaries
…able_with_cantor_image - Replace sublevel_set_measurable sorry with proof structure: extract real from EReal, define S, show convexity via MonotoneOn.convex_le, show boundedness - Complete exists_nonmeasurable_with_cantor_image proof: show F = VitaliSet ∩ A is non-measurable by contradiction using VitaliSet.nonmeasurable - Enhance example final sorry with detailed proof sketch for preimage argument using injectivity - Refactor VitaliSet.nonmeasurable into separate theorem in Section_1_2_3.lean for reusability
…ation
- Change BinaryToTernaryProperties: bijective_on_nonterminating → injective_on_nonterminating
- Add binaryDigit function: extracts j-th binary digit using floor and mod
- Add binaryToTernaryFn: implements g(x) = ∑ 2·bⱼ(x)·3^{-j} for x ∈ [0,1]
- Add helper lemmas: binaryDigit bounds, zero/one cases, summability, geometric series
- Add DyadicRationals definition and countability proof
- Add floor manipulation lemmas for monotonicity proof (floor_two_mul_odd_ge, etc.)
- Start binaryToTernary_props proof: nonneg, bounded, zero_outside, zero_at_zero, zero_set_countable, monotone_on, image_in_cantor, injective_on_nonterminating (partial, has sorry)
- Update references from bijective_on_nonterminating to injective_on_nonterminating
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Remark 1.3.10 implementation (partial): Add binary digit extraction machinery (binaryDigit, binaryToTernaryFn). Complete f_zero_set_measurable proof decomposing zero set into open and countable parts. Complete sublevel_set_measurable proof structure using convexity. Complete exists_nonmeasurable_with_cantor_image showing F = VitaliSet ∩ A is non-measurable. Refactor VitaliSet.nonmeasurable into reusable theorem. Update BinaryToTernaryProperties to use injective_on_nonterminating. Add helper lemmas for binary digits, dyadic rationals, and floor manipulations.