TestedTransport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceSamplingRectangle line 10
theorem OAI.FiniteFactor.sourceSamplingRectangle_measurable line 14
theorem OAI.FiniteFactor.sourceSamplingProduct_first_indicator line 23

theorem OAI.FiniteFactor.sourceSamplingProduct_second_inverse line 49

Source documentation

Inverse rotation exchanges the two actual tested product orientations.

theorem sourceSamplingProduct_second_inverse (I : Finset SourceCoordinate) (stage : ℕ)
    (E G : SourceCoordinate → Set ℝ) (θ y : SourceCoordinate → ℝ) (n : ℤ)
    (hy : ∀ i, y i ∈ Set.Ico (0 : ℝ) 1) :
    sourceSamplingProduct stage false (fun i => decide (i ∈ I)) E G n θ
      (coordinateRotate θ (-n) y) =
    sourceSamplingProduct stage true (fun i => decide (i ∈ I)) E G n θ y := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingProduct, OAI.FiniteFactor.coordinateRotate

theorem OAI.FiniteFactor.sourceSamplingSummand_restrict_rectangle line 66

Source documentation

The restricted orbit-pair summand is exactly the pushforward of its first tested product, with no assumed marginal law.

theorem sourceSamplingSummand_restrict_rectangle (I : Finset SourceCoordinate) (stage : ℕ)
    (E G : SourceCoordinate → Set ℝ)
    (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i))
    (houtside : ∀ i ∉ sourceSamplingPrefix stage,
      Set.Ico (0 : ℝ) 1 ⊆ E i ∧ Set.Ico (0 : ℝ) 1 ⊆ G i)
    (θ : SourceCoordinate → ℝ) (n : ℤ) :
    (sourceSamplingSummand I stage θ n).restrict (sourceSamplingRectangle E G) =
      (sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal
        (sourceSamplingProduct stage false (fun i => decide (i ∈ I)) E G n θ x))).map
          (fun x => (x,coordinateRotate θ n x)) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.sourceSamplingSummand, OAI.FiniteFactor.sourceSamplingRectangle, OAI.FiniteFactor.sourceSamplingProduct, OAI.FiniteFactor.coordinateRotate