OccupationSampling.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual probability laws of independent chart samples

def OAI.PolycyclicRecognition.cellProbabilityMeasure line 17

Source documentation

Uniform sampling from an actual measurable cell of positive finite mass.

def cellProbabilityMeasure {Z : Type*} [MeasurableSpace Z]
    (μ : Measure Z) (S : Set Z) (hzero : μ S ≠ 0) (hfin : μ S ≠ ⊤) :
    ProbabilityMeasure Z :=
…

theorem OAI.PolycyclicRecognition.integral_cellProbabilityMeasure line 25

def OAI.PolycyclicRecognition.densityProbabilityMeasure line 35

Source documentation

A nonnegative integrable density of mass one defines a probability.

def densityProbabilityMeasure {Z : Type*} [MeasurableSpace Z]
    (μ : Measure Z) (ρ : Z → ℝ) (hi : Integrable ρ μ)
    (hp : ∀ z, 0 ≤ ρ z) (hmass : ∫ z, ρ z ∂μ = 1) : ProbabilityMeasure Z :=
…

theorem OAI.PolycyclicRecognition.integral_densityProbabilityMeasure line 46

Source documentation

Integrating against that probability is the ordinary density-weighted integral, including for scale-dependent observables.

theorem integral_densityProbabilityMeasure
    {Z : Type*} [MeasurableSpace Z]
    (μ : Measure Z) (ρ : Z → ℝ) (hi : Integrable ρ μ)
    (hp : ∀ z, 0 ≤ ρ z) (hmass : ∫ z, ρ z ∂μ = 1)
    (f : Z → ℝ) :
    (∫ z, f z ∂(densityProbabilityMeasure μ ρ hi hp hmass : Measure Z)) =
      ∫ z, ρ z * f z ∂μ := by
…

Mentions: OAI.PolycyclicRecognition.densityProbabilityMeasure

theorem OAI.PolycyclicRecognition.ae_mem_densityProbabilityMeasure line 61

Source documentation

A density sample lies almost surely in every set outside which the density vanishes. In particular its compact support carries the law.

theorem ae_mem_densityProbabilityMeasure
    {Z : Type*} [MeasurableSpace Z]
    (μ : Measure Z) (ρ : Z → ℝ) (hi : Integrable ρ μ)
    (hp : ∀ z, 0 ≤ ρ z) (hmass : ∫ z, ρ z ∂μ = 1)
    (K : Set Z) (hK : ∀ z, z ∉ K → ρ z = 0) :
    ∀ᵐ z ∂(densityProbabilityMeasure μ ρ hi hp hmass : Measure Z), z ∈ K := by
…

Mentions: OAI.PolycyclicRecognition.densityProbabilityMeasure

def OAI.PolycyclicRecognition.productOccupationLaw line 74

Source documentation

The law of a measurable chart sampled independently in its two factors.

def productOccupationLaw {A D X : Type*}
    [MeasurableSpace A] [MeasurableSpace D] [MeasurableSpace X]
    (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D) (p : A × D → X) :
    ProbabilityMeasure X :=
…

theorem OAI.PolycyclicRecognition.integral_productOccupationLaw line 82

Source documentation

Fubini's formula for a bounded continuous observable of a chart sample.

theorem integral_productOccupationLaw
    {A D X : Type*} [MeasurableSpace A] [MeasurableSpace D]
    [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X]
    (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D)
    (p : A × D → X) (hp : Measurable p) (f : C(X, ℝ)) :
    (∫ x, f x ∂(productOccupationLaw μ ν p : Measure X)) =
      ∫ a, ∫ d, f (p (a, d)) ∂(ν : Measure D) ∂(μ : Measure A) := by
…

Mentions: OAI.PolycyclicRecognition.productOccupationLaw

theorem OAI.PolycyclicRecognition.integral_productOccupationLaw_symm line 96

Source documentation

The same formula with the other factor outside.

theorem integral_productOccupationLaw_symm
    {A D X : Type*} [MeasurableSpace A] [MeasurableSpace D]
    [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X]
    (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D)
    (p : A × D → X) (hp : Measurable p) (f : C(X, ℝ)) :
    (∫ x, f x ∂(productOccupationLaw μ ν p : Measure X)) =
      ∫ d, ∫ a, f (p (a, d)) ∂(μ : Measure A) ∂(ν : Measure D) := by
…

Mentions: OAI.PolycyclicRecognition.productOccupationLaw

theorem OAI.PolycyclicRecognition.productOccupationLaw_error_eq line 111

Source documentation

Exact translated-law error formula. In particular, estimates only on the support of the second sampling measure suffice after this identity.

theorem productOccupationLaw_error_eq
    {A D X G : Type*} [MeasurableSpace A] [MeasurableSpace D]
    [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X]
    [SMul G X] [ContinuousConstSMul G X]
    (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D)
    (p : A × D → X) (hp : Measurable p) (g : G) (f : C(X, ℝ)) :
    (∫ x, f (g • x) ∂(productOccupationLaw μ ν p : Measure X)) -
        ∫ x, f x ∂(productOccupationLaw μ ν p : Measure X) =
      ∫ d, ((∫ a, f (g • p (a, d)) ∂(μ : Measure A)) -
        ∫ a, f (p (a, d)) ∂(μ : Measure A)) ∂(ν : Measure D) := by
…

Mentions: OAI.PolycyclicRecognition.productOccupationLaw