SecondMarginal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceSamplingSummand_second_density line 13
Source documentation
The actual second marginal of one orbit summand, obtained by weighted Haar transport and not supplied as an assumption.
```
theorem sourceSamplingSummand_second_density (I : Finset SourceCoordinate) (stage : ℕ)
    (θ : SourceCoordinate → ℝ) (n : ℤ) :
    (sourceSamplingSummand I stage θ n).map Prod.snd =
      sourceSamplingHaar.withDensity (fun y => ENNReal.ofReal
        (sourceSamplingWeight I stage θ n (coordinateRotate θ (-n) y))) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingSummand, OAI.FiniteFactor.sourceSamplingWeight, OAI.FiniteFactor.coordinateRotate

theorem OAI.FiniteFactor.sourceSamplingUntrimmed_second_density line 26

Source documentation

The actual second marginal is the second-oriented empirical density.

theorem sourceSamplingUntrimmed_second_density (I : Finset SourceCoordinate) (stage : ℕ)
    (θ : SourceCoordinate → ℝ) :
    (sourceSamplingUntrimmed I stage θ).map Prod.snd =
      sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal
        (sourceSamplingEmpiricalDensity stage true (fun i => decide (i ∈ I))
          (fun _ => Set.Icc 0 1) (fun _ => Set.Icc 0 1) θ x)) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingEmpiricalDensity

theorem OAI.FiniteFactor.sourceSamplingUntrimmed_second_L2 line 67

Source documentation

Uniform L2 densities for the actual untrimmed second marginals.

theorem sourceSamplingUntrimmed_second_L2 (I : Finset SourceCoordinate) :
    ∀ᵐ θ ∂sourceAngleLaw, ∃ C : ℝ, ∀ stage,
      ∃ f : (SourceCoordinate → ℝ) → ℝ,
        (sourceSamplingUntrimmed I stage θ).map Prod.snd = sourceSamplingHaar.withDensity (fun x => ENNReal.ofReal (f x)) ∧
        MemLp f 2 sourceSamplingHaar ∧ (∫ x, f x^2 ∂sourceSamplingHaar) ≤ C := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingHaar