ProbeCellVolume.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive probe probabilities give actual endpoint volume

theorem OAI.PolycyclicRecognition.cellProbabilityMeasure_prod line 16

Source documentation

Independent uniform sampling on two finite cells is uniform sampling on their product, with the exact product Haar normalization.

theorem cellProbabilityMeasure_prod
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) [SFinite μ] [SFinite ν]
    (A : Set X) (B : Set Y) (hA0 : μ A ≠ 0) (hAt : μ A ≠ ⊤)
    (hB0 : ν B ≠ 0) (hBt : ν B ≠ ⊤) :
    (cellProbabilityMeasure μ A hA0 hAt : Measure X).prod
        (cellProbabilityMeasure ν B hB0 hBt : Measure Y) =
      ((μ.prod ν) (A ×ˢ B))⁻¹ • (μ.prod ν).restrict (A ×ˢ B) := by
…

Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure

theorem OAI.PolycyclicRecognition.probe_cell_image_volume_lower line 30

Source documentation

A positive fraction of the original cell becomes a corresponding amount of actual volume under the section-coordinate embedding.

theorem probe_cell_image_volume_lower
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (e : X → Y) (he : MeasurableEmbedding e)
    (A K : Set X) (hA0 : μ A ≠ 0) (hAt : μ A ≠ ⊤)
    (hK : MeasurableSet K) (hKA : K ⊆ A)
    {c : ℝ} (hc : 0 ≤ c)
    (hmass : ENNReal.ofReal c ≤ (cellProbabilityMeasure μ A hA0 hAt : Measure X) K) :
    c * (μ A).toReal ≤ ((Measure.map e μ) (e '' K)).toReal := by
…

Mentions: OAI.PolycyclicRecognition.cellProbabilityMeasure