CappedTransfer.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.SourceOrderedTorusSampling.uniformAC line 16
Source documentation
Uniform absolute continuity of both actual ordered sampling marginals, derived from the previously proved L2 density bounds.
```
theorem SourceOrderedTorusSampling.uniformAC {θ : SourceCoordinate → ℝ}
    (hθ : SourceOrderedTorusSampling θ) (I : Finset SourceCoordinate) (r : Bool)
    (ε : ℝ≥0) (hε : 0 < ε) :
    ∃ δ : ℝ≥0∞, 0 < δ ∧ ∀ A, MeasurableSet A → sourceTorusHaar A < δ → ∀ n,
      ((sourceSamplingTrimmedTorus I n θ : Measure SourceSamplingTorus).map
        (sourceTorusEndpoint r)) A ≤ ε := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceSamplingTrimmedTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusEndpoint
theorem OAI.FiniteFactor.sourceCappedPair_limit_transfer line 31
Source documentation
The actual capped projection equation passes to lambda_I on the original sampling torus. The approximant equations are the remaining orbit obligation; no continuity or measurable-selection premise is assumed.
```
theorem sourceCappedPair_limit_transfer {θ : SourceCoordinate → ℝ}
    (hθ : SourceOrderedTorusSampling θ) (I : Finset SourceCoordinate)
    (H : SourceHilbert SourceCoordinate →L[ℂ] SourceHilbert SourceCoordinate)
    (hpair : ∀ n, ∀ᵐ z ∂(sourceSamplingTrimmedTorus I n θ : Measure SourceSamplingTorus),
      z ∈ sourceCappedPairZeroSet θ H) :
    ∀ᵐ z ∂(sourceSamplingLambdaTorus I : Measure SourceSamplingTorus),
      z ∈ sourceCappedPairZeroSet θ H := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceOrderedTorusSampling, OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.sourceSamplingTrimmedTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceCappedPairZeroSet, OAI.FiniteFactor.sourceSamplingLambdaTorus