LocalBranchMeasure.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem356.LocalBranchMeasure.extendedBranch line 18
Source documentation
A local branch extended by a fixed value outside its source.
```
def extendedBranch (e : OpenPartialHomeomorph α β) (z : β) : α → β := by
…
```
theorem OAI.Problem356.LocalBranchMeasure.extendedBranch_apply_of_mem line 23
theorem OAI.Problem356.LocalBranchMeasure.measurable_extendedBranch line 30
Source documentation
The extension is Borel measurable even if the local map is arbitrary outside its source.
```
theorem measurable_extendedBranch (e : OpenPartialHomeomorph α β) (z : β) :
    Measurable (extendedBranch e z) := by
…
```
Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch
theorem OAI.Problem356.LocalBranchMeasure.measurableSet_image line 37
Source documentation
Restricting the domain of a local branch to a measurable set gives a measurable image.
```
theorem measurableSet_image (e : OpenPartialHomeomorph α β)
    {S : Set α} (hS : MeasurableSet S) (hSub : S ⊆ e.source) :
    MeasurableSet (e '' S) := by
…
```
theorem OAI.Problem356.LocalBranchMeasure.extendedBranch_image line 46
Source documentation
Extension preserves every image of a subset of the local source.
```
theorem extendedBranch_image (e : OpenPartialHomeomorph α β) (z : β)
    {S : Set α} (hSub : S ⊆ e.source) :
    extendedBranch e z '' S = e '' S := by
…
```
Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch
theorem OAI.Problem356.LocalBranchMeasure.measurableSet_extendedBranch_image line 54
Source documentation
Measurability of selected branch images required by deterministic-selection obstructions.
```
theorem measurableSet_extendedBranch_image (e : OpenPartialHomeomorph α β) (z : β)
    {S : Set α} (hS : MeasurableSet S) (hSub : S ⊆ e.source) :
    MeasurableSet (extendedBranch e z '' S) := by
…
```
Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch
theorem OAI.Problem356.LocalBranchMeasure.injOn_extendedBranch line 62
Source documentation
Injectivity of the extension on any subset of the source.
```
theorem injOn_extendedBranch (e : OpenPartialHomeomorph α β) (z : β)
    {B : Set α} (hB : B ⊆ e.source) : InjOn (extendedBranch e z) B := by
…
```
Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch
theorem OAI.Problem356.LocalBranchMeasure.map_extendedBranch line 71
Source documentation
Extending outside the source does not change pushforwards of measures concentrated there.
```
theorem map_extendedBranch (e : OpenPartialHomeomorph α β) (z : β)
    (ν : Measure α) (hν : ∀ᵐ x ∂ν, x ∈ e.source) :
    Measure.map (extendedBranch e z) ν = Measure.map e ν := by
…
```
Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch

theorem OAI.Problem356.LocalBranchMeasure.measurableSet_selection line 79

Source documentation

A measurable selector's coincidence set with an extended local branch is measurable.

theorem measurableSet_selection [MeasurableEq β]
    (e : OpenPartialHomeomorph α β) (z : β) {B : Set α}
    (hB : MeasurableSet B) {T : α → β} (hT : Measurable T) :
    MeasurableSet (B ∩ {x | T x = extendedBranch e z x}) :=
…

Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch

theorem OAI.Problem356.LocalBranchMeasure.measurableSet_selection_image line 86

Source documentation

Selected coincidence sets have measurable branch images.

theorem measurableSet_selection_image [MeasurableEq β]
    (e : OpenPartialHomeomorph α β) (z : β) {B : Set α}
    (hB : MeasurableSet B) (hSub : B ⊆ e.source)
    {T : α → β} (hT : Measurable T) :
    MeasurableSet (extendedBranch e z '' (B ∩ {x | T x = extendedBranch e z x})) := by
…

Mentions: OAI.Problem356.LocalBranchMeasure.extendedBranch