DiagonalLoss.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.positive_small_sets_tendsto line 13

Source documentation

Positive measurable functions have vanishing mass below the actual source threshold 1/(j+1), without any quantitative lower bound.

theorem positive_small_sets_tendsto {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ] (r : X → ℝ) (hr : Measurable r)
    (hpos : ∀ᵐ x ∂μ, 0 < r x) :
    Tendsto (fun j : ℕ => μ.real {x | r x < 1/((j : ℝ)+1)}) atTop (𝓝 0) := by
…

theorem OAI.FiniteFactor.sourceBiased_positive_endpoint_loss line 39
Source documentation
The actual uniformly L2-bounded biased marginals inherit that vanishing loss even though their full infinite-dimensional densities vary with j.
```
theorem sourceBiased_positive_endpoint_loss (r : (SourceCoordinate → ℝ) → ℝ)
    (hr : Measurable r) (hpos : ∀ᵐ x ∂sourceBaseMeasure, 0 < r x) (b : Bool) :
    Tendsto (fun j : ℕ => (sourceBiasedLaw j).real
      {ω | r (sourceBiasedEndpoint (fun _ => b) ω) < 1/((j : ℝ)+1)}) atTop (𝓝 0) := by
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceBaseMeasure, OAI.FiniteFactor.sourceBiasedLaw, OAI.FiniteFactor.sourceBiasedEndpoint