OAI/GroupTheory/PolycyclicRecognition/Analysis/CompactProbabilityProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.productOccupationLaw_map_left line 16

   Source documentation

   Pushing forward the first independent coordinate is the same as pushing the joint law through the corresponding product map.

   theorem productOccupationLaw_map_left
       {A B D : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace D]
       (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D)
       (f : A → B) (hf : Measurable f) :
       productOccupationLaw (ProbabilityMeasure.map μ f) ν id =
         productOccupationLaw μ ν (Prod.map f id) := by
   …

   Mentions: OAI.PolycyclicRecognition.productOccupationLaw

2. theorem OAI.PolycyclicRecognition.continuous_integral_compact_function line 30

   Source documentation

   Integration against a probability is continuous in the uniform norm.

   theorem continuous_integral_compact_function
       {X : Type*} [TopologicalSpace X] [CompactSpace X]
       [MeasurableSpace X] [BorelSpace X] (μ : ProbabilityMeasure X) :
       Continuous (fun f : C(X, ℝ) => ∫ x, f x ∂(μ : Measure X)) := by
   …

3. theorem OAI.PolycyclicRecognition.productOccupationLaw_tendsto_fixed line 48

   Source documentation

   A fixed independent coordinate preserves weak convergence of the profile law. No rate in the other coordinate is required.

   theorem productOccupationLaw_tendsto_fixed
       {A D ι : Type*} [TopologicalSpace A] [CompactSpace A]
       [TopologicalSpace D] [CompactSpace D] [SecondCountableTopology D]
       [MeasurableSpace A] [BorelSpace A] [MeasurableSpace D] [BorelSpace D]
       {l : Filter ι} (μs : ι → ProbabilityMeasure A) (μ : ProbabilityMeasure A)
       (hμ : Tendsto μs l (𝓝 μ)) (ν : ProbabilityMeasure D) :
       Tendsto (fun i => productOccupationLaw (μs i) ν id) l
         (𝓝 (productOccupationLaw μ ν id)) := by
   …

   Mentions: OAI.PolycyclicRecognition.productOccupationLaw

4. theorem OAI.PolycyclicRecognition.mem_support_productOccupationLaw line 68

   Source documentation

   Every pair of supported points is supported by independent sampling.

   theorem mem_support_productOccupationLaw
       {A D : Type*} [TopologicalSpace A] [TopologicalSpace D]
       [MeasurableSpace A] [MeasurableSpace D]
       (μ : ProbabilityMeasure A) (ν : ProbabilityMeasure D)
       {a : A} {d : D} (ha : a ∈ (μ : Measure A).support)
       (hd : d ∈ (ν : Measure D).support) :
       (a, d) ∈ (productOccupationLaw μ ν id : Measure (A × D)).support := by
   …

   Mentions: OAI.PolycyclicRecognition.productOccupationLaw