OAI/Analysis/FiniteFactor/Sampling/WeightedCoordinate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.weighted_prefix_coordinate_mass line 13

   Source documentation

   Exact relative mass of a tail-coordinate event under a prefix product weight. This includes zero-mass weights and requires no division by mass.

   theorem weighted_prefix_coordinate_mass {ι : Type*} [DecidableEq ι]
       (μi : ι → Measure ℝ) [∀ i, IsProbabilityMeasure (μi i)]
       (J : Finset ι) (F : ι → ℝ → ℝ≥0∞) (hF : ∀ j, Measurable (F j))
       (i : ι) (hi : i ∉ J) (E : Set ℝ) (hE : MeasurableSet E) :
       ((Measure.infinitePi μi).withDensity (fun x => ∏ j ∈ J, F j (x j))) {x | x i ∈ E} =
         ((Measure.infinitePi μi).withDensity (fun x => ∏ j ∈ J, F j (x j))) Set.univ * μi i E := by
   …

2. theorem OAI.FiniteFactor.sourceSampling_tail_coordinate_mass line 63

   Source documentation

   The source sampling summand has exactly the Haar tail-coordinate probability multiplied by its own mass.

   theorem sourceSampling_tail_coordinate_mass (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) (n : ℤ) (i : SourceCoordinate) (hi : s < i.1)
       (E : Set ℝ) (hE : MeasurableSet E) :
       sourceSamplingWeightedMeasure I s θ n {x | x i ∈ E} =
         sourceSamplingWeightedMeasure I s θ n Set.univ * unitIntervalMeasure E := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingWeightedMeasure, OAI.FiniteFactor.unitIntervalMeasure