Add Theorems on Infimum Function Domains and Supporting Results #4616
Conversation
This file contains 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
- Reduced constraints by replacing them with 'effectively not free' hypotheses. - Improves theorem usability and simplifies certain dependencies.
This commit includes: - Theorems specific to sigma-algebras about the |`t operator. - Theorems specific to topologies about the |`t operator. - General theorems about the |`t operator. Additionally, variations of existing theorems have been added: - Deduction versions (e.g., ~ inopnd). - 'Effectively not free' versions (e.g., ~ ss2rabdf).
This commit introduces four theorems related to the domains of function addition and multiplication within the context of sigma-algebras: Theorems adddmmbl and adddmmbl2: If two functions have domains in a sigma-algebra, the domain of their addition also belongs to the sigma-algebra. These theorems correspond to the first statement of Proposition 121H from [Fremlin1], p. 39. The assumption of sigma-measurability for the functions, as in the original text, is not required here. Theorems muldmmbl and muldmmbl2: Similarly, if two functions have domains in a sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. These theorems correspond to the second statement of Proposition 121H from [Fremlin1], p. 39, again without requiring sigma-measurability. This commit also adds four missing full stops in previously committed comments.
…nd measurable functions This commit introduces some new theorems to set.mm, including contributions related to subclass relationships, domains of mappings, functionality, and sigma-algebra measurable functions. These include: Subclass of a restricted class abstraction (deduction form): ssrabdf Domain of the mapping operation (deduction form): dmmpt1 Functionality of the mapping operation: fmptff Function value and codomain relationship: fvmptelcdmf Mapping operation with bound-variable hypothesis: fmptdff Function measurability in sigma-algebras: smffmptf: Demonstrates measurability as a function. smfdmmblpimne: Predomain of 'all but one' of measurable functions in sigma-algebras. smfdivdmmbl: Domain of a division of measurable functions in sigma-algebras. smfdivdmmbl2: Variant of smfdivdmmbl using function notation. smfpimne: Preimage of reals different from a given value in a subspace sigma-algebra. smfpimne2: Variant of smfpimne with the extended real assumption relaxed to existence.
This commit introduces two main theorems and supporting results: 1. **Equality result for the domain of the sup function**: Derived from Proposition 121F(b) and used in the proof of Proposition 121H of [Fremlin1], this theorem establishes a general framework for the sup function without requiring sigma-measurability. 2. **Supremum function in sigma-algebras**: If a countable set of sigma-measurable functions have domains in the sigma-algebra, their supremum function also has its domain in the sigma-algebra, as described in Proposition 121H of [Fremlin1]. Additionally, the commit includes: - Properties of sigma-algebras, including closure under indexed unions and intersections. - Restricted quantification principles and subset relations for indexed operations. - Foundational results, such as natural numbers as extended reals and expressions for the empty set.
- Corrected "thei" to "their" - Rephrased "an operation" to "a function"
Infimum Function Domain: Added theorems ~ finfdm, ~ finfdm2, and ~ smfinfdmmbl, formalizing key results on the domain of the infimum function. These results clarify the measurability and domain properties of the infimum function in measure theory, specifically: - finfdm, finfdm2: alternative definitions for the domain of the infimum function. - smfinfdmmbl: Prove that if a countable set of sigma-measurable functions have domains in a sigma-algebra, their infimum function's domain is also in the sigma-algebra. This is the fifth statement of Proposition 121H in [Fremlin1], p. 39.
|
mathbox only |
icecream17
approved these changes
Feb 1, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
This PR introduces theorems related to the domain of the infimum function, along with a supporting result for the Archimedean property of real numbers.
Key Contributions:
Results on Infimum Function Domains:
finfdm,finfdm2: alternative definitions for the domain of the infimum function, as per Proposition 121F (c) of [Fremlin1], p. 39, and the proof of Proposition 121H in [Fremlin1].smfinfdmmbl: Prove that if a countable set of sigma-measurable functions have domains in a sigma-algebra, their infimum function's domain is also in the sigma-algebra. This is the fifth statement of Proposition 121H in [Fremlin1], p. 39.Supporting Theorem:
archd: Proves the Archimedean property of real numbers, a foundational result used as a helper in the proofs of the main theorems.