Complete Remark 1.3.10 proof and absolute integrability results #431
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
- Section_1_2_2: Fix CantorInterval exponent from (n+1) to n - Section_1_3_2: Refactor Remark 1.3.10 with simplified strategy docs, add DyadicRationals definition and countability proof, clarify implementation differences from textbook, update BinaryToTernaryProperties structure
- Relax binaryDigit_partial_sum_lt signature (remove Ico constraint), update call sites - Fix sum_add_tsum_nat_add calls to use Summable.sum_add_tsum_nat_add - Complete Remark 1.3.10 example proof: show A' measurable via complement of countable set, then F' = f⁻¹(E) ∩ A' is measurable intersection - Rename f to f_lifted and update related lemma names for clarity - Use underscore prefix for unused hypothesis names
- Move geometric series and floor helper lemmas (tsum_two_thirds_geometric, tsum_tail_bound, floor_two_mul_odd_ge, floor_two_mul_even_le, floor_two_mul_eq_of_mod_eq) before Remark_1_3_10 namespace - Remove BinaryToTernaryProperties structure and binaryToTernaryFn definition (unused) - Simplify DyadicRationals comment - Clean up proof structure and organization
- Complete RealMeasurable.iff: prove equivalence between RealMeasurable and ComplexMeasurable for real functions using simple function approximations and continuity - Complete ComplexMeasurable.iff: prove equivalence between ComplexMeasurable and RealMeasurable for real/imaginary parts, constructing complex simple functions from real ones
….abs proofs - Complete ComplexAbsolutelyIntegrable.abs: prove that absolute value of complex absolutely integrable function is unsigned absolutely integrable, using measurability and continuity of norm - Complete RealAbsolutelyIntegrable.abs: prove that absolute value of real absolutely integrable function is unsigned absolutely integrable, using same approach with real norm
- Complete RealAbsolutelyIntegrable.iff: prove equivalence with ComplexAbsolutelyIntegrable for real functions using norm equality - Complete ComplexAbsolutelyIntegrable.re/im: prove real/imaginary parts of complex absolutely integrable functions are real absolutely integrable, using measurability and integral monotonicity - Complete ComplexAbsolutelyIntegrable.iff: prove equivalence with both parts being absolutely integrable, using triangle inequality bound |f| ≤ |Re(f)| + |Im(f)| and integral additivity
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.
Summary
This PR completes the formalization of Remark 1.3.10 and adds absolute integrability results:
Bug fix:
Remark 1.3.10 completion:
Updates on Jan12:
Files changed: Section_1_2_2.lean, Section_1_3_2.lean, Section_1_3_4.lean