Complete Lemma 1.3.9 TFAE proof and refactorings #425
Merged
+1,472
−56
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
- Complete ix_imp_x: prove open sets are countable unions of intervals via decomposition into ℝ, {⊤}, {⊥} parts
- Add helper lemmas: unsigned_preimage_bot_empty, ereal_reals_eq_iUnion, measurable_preimage_reals, ereal_top_singleton_eq, measurable_preimage_top, open_inter_reals_eq_countable_union
- Add structure for v_to_xi_imp_iv: define truncate_at, discretize, approx_seq helper functions and proof framework
- Update TFAE proof to pass Unsigned f hypothesis to ix_imp_x
- Several technical details in v_to_xi_imp_iv marked with sorry (simple function construction, monotonicity, convergence)
- Refactor all statement abbreviations and proofs to use LebesgueMeasurable instead of MeasurableSet
- Update proofs to use LebesgueMeasurable API: complement, inter, countable_union, countable_inter
- Refactor vi_imp_v to use Encodable ℚ for proper countable union encoding
- Refactor ix_imp_x to use Encodable S for countable union over interval sets
- Complete approx_fn definition: discretization function for approximating sequence
- Add approx_fn_values lemma: shows approx_fn takes values in {k/2^n : k ≤ n·2^n}
- Add approx_fn_levelset_LebesgueMeasurable: proves level sets are Lebesgue measurable via Boolean combinations of measurable sets
- Add helper lemmas: mul_pow2_div_pow2_eq, ereal_div_pow2_eq_imp_eq for arithmetic properties
- Complete iii_imp_v: prove {f > t} is Lebesgue measurable via limsup representation and almost-everywhere equality
- Add helper lemmas: LebesgueMeasurable.finset_inter, finset_union for finite set operations
- Add Set.indicator'_eq_one' and indicator'_eq_zero' for indicator function properties
- Add UnsignedSimpleFunction.levelset_gt_LebesgueMeasurable: level sets of simple functions are measurable via atom decomposition
- Add limsupSet definition and limsupSet_LebesgueMeasurable lemma
- Add IsNull.subset and LebesgueMeasurable.of_ae_eq for almost-everywhere equality arguments
- Proof strategy: show {f > t} equals limsupSet outside null set, use convergence properties to establish equality
- Add helper lemmas: approx_fn_nonneg, floor_approx_iSup_eq, approx_fn_eq_floor_when_finite - Complete monotonicity proof: show approx_fn f m x ≤ approx_fn f n x when m ≤ n via floor approximation properties - Start convergence proof: show f x = iSup (approx_fn f · x) with case analysis for f x = ⊤ and f x < ⊤ - Proof uses floor approximation properties and eventually |x| ≤ n for convergence
- Remove unnecessary not_and from simp only in limsupSet_LebesgueMeasurable - Remove redundant hd from simp only in vi_imp_v and ix_imp_x - Mark hv as unused (_hv) in v_to_xi_imp_iv since it's not used in the proof
- Move IsNull.subset, LebesgueMeasurable.finset_inter, finset_union, of_ae_eq, closedBall from private namespace in Section_1_3_2.lean to public space in Section_1_2_2.lean - Remove private versions from Section_1_3_2.lean and update references to use public lemmas - Improves code organization by placing general measure theory lemmas in appropriate section
- Remove redundant hypotheses from simp only calls (h1, h2, h3, hk_coe, h2n_coe) that simp already handles - Mark unused variables in v_to_xi_imp_iv as _hviii, _hix, _hx, _hxi - Remove unnecessary approx_fn from simp call in approx_fn_levelset_LebesgueMeasurable - Simplify Fin.mk.injEq to just simp only in v_to_xi_imp_iv
- Remove unused parameters _hv, _hviii, _hix, _hx, _hxi from v_to_xi_imp_iv signature - Keep only hf, hvi, hvii which are actually used in the proof - Simplify call site in TFAE proof to only pass necessary arguments - Eliminates unused variable warnings
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
Completed Lemma 1.3.9 (Equivalent notions of measurability) TFAE proof with all implications. Refactored general lemmas to Section_1_2_2. Completed proofs for simple functions, almost-everywhere equality, and approximating sequences. Added helper lemmas for Lebesgue measurability operations. Cleaned up unused parameters and simplified proof tactics.
Key changes: