TrimmedMarginals.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSamplingTrimmed_marginal_le line 13
Source documentation
Each actual trimmed marginal is dominated by the actual untrimmed marginal, for both orientations.
```
theorem sourceSamplingTrimmed_marginal_le (I : Finset SourceCoordinate) (s : ℕ)
    (θ : SourceCoordinate → ℝ) (r : Bool) :
    (sourceSamplingTrimmed I s θ).map (sourceSamplingEndpoint r) ≤
      (sourceSamplingUntrimmed I s θ).map (sourceSamplingEndpoint r) :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingTrimmed, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingUntrimmed

theorem OAI.FiniteFactor.sourceSamplingTrimmed_marginals_event line 21

Source documentation

The actual Radon--Nikodym densities after trimming have the same uniform squared L2 bound, on a single event for every finite I and both endpoints.

theorem sourceSamplingTrimmed_marginals_event : ∀ᵐ θ ∂sourceAngleLaw,
    ∀ (I : Finset SourceCoordinate) (r : Bool), ∃ C : ℝ, ∀ s : ℕ,
      ∃ g : (SourceCoordinate → ℝ) → ℝ,
        Measurable g ∧ (∀ x, 0 ≤ g x) ∧
        (sourceSamplingTrimmed I s θ).map (sourceSamplingEndpoint r) =
          sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal (g x)) ∧
        MemLp g 2 sourceSamplingHaar ∧ (∫ x, g x^2 ∂sourceSamplingHaar) ≤ C := by
…

Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingTrimmed, OAI.FiniteFactor.sourceSamplingEndpoint, OAI.FiniteFactor.sourceSamplingHaar