NormalizedEndpointMeasure.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Normalized measure on an independent endpoint domain

Normalizing the restricted coordinate measure produces a probability on the endpoint subtype. A bad set of probability below one half leaves at least half of the original coordinate volume.

def OAI.PolycyclicRecognition.normalizedEndpointMeasure line 23
Source documentation
Probability normalization on the endpoint subtype.
```
def normalizedEndpointMeasure (μ : Measure V) (S : Set V) : Measure S :=
…
```
theorem OAI.PolycyclicRecognition.normalizedEndpointMeasure_isProbability line 26

theorem OAI.PolycyclicRecognition.endpoint_volume_eq_mass_mul_probability line 35

Source documentation

Recover original coordinate volume from the normalized probability.

theorem endpoint_volume_eq_mass_mul_probability (μ : Measure V) {S : Set V}
    (hS : MeasurableSet S) (h₀ : μ S ≠ 0) (hfin : μ S ≠ ⊤) (A : Set S) :
    μ (Subtype.val '' A) = μ S * normalizedEndpointMeasure μ S A := by
…

Mentions: OAI.PolycyclicRecognition.normalizedEndpointMeasure

theorem OAI.PolycyclicRecognition.half_volume_le_good_endpoints line 42

Source documentation

The good endpoints retain half the original coordinate mass.

theorem half_volume_le_good_endpoints (μ : Measure V) {S : Set V}
    (hS : MeasurableSet S) (h₀ : μ S ≠ 0) (hfin : μ S ≠ ⊤)
    {B : Set S} (hB : MeasurableSet B)
    (hbad : normalizedEndpointMeasure μ S B < 1 / 2) :
    μ S * (1 / 2) ≤ μ (Subtype.val '' Bᶜ) := by
…

Mentions: OAI.PolycyclicRecognition.normalizedEndpointMeasure