DiagonalContribution.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.sourceSamplingDiagonalContribution line 10
Source documentation
The self-pair part of the empirical squared norm, with its actual P^-2 weight.
```
def sourceSamplingDiagonalContribution (stage : ℕ) (r : Bool) (b : SourceCoordinate → Bool)
    (E G : SourceCoordinate → Set ℝ) (θ : SourceCoordinate → ℝ) : ℝ :=
…
```
Mentions: OAI.FiniteFactor.SourceCoordinate
theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_nonneg line 16
theorem OAI.FiniteFactor.sourceSamplingProduct_square_integrable line 21
theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_integrable line 31
theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_expectation line 40
Source documentation
The diagonal contribution's expectation is bounded by the proved summable budget; the finite set is the actual deterministic sample set.
```
theorem sourceSamplingDiagonalContribution_expectation (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
    (r : Bool) (b : SourceCoordinate → Bool) (E G : SourceCoordinate → Set ℝ)
    (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
    (∫ θ, sourceSamplingDiagonalContribution stage r b E G θ ∂sourceAngleLaw) ≤ sourceSamplingSelfBudget stage := by
…
```
Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingDiagonalContribution, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceSamplingSelfBudget

theorem OAI.FiniteFactor.sourceSamplingDiagonalContribution_summable_integral line 58

Source documentation

Actual self-pair expectations are summable across the constructed stages.

theorem sourceSamplingDiagonalContribution_summable_integral (r : Bool) (b : SourceCoordinate → Bool)
    (E G : SourceCoordinate → Set ℝ) (hE : ∀ i, MeasurableSet (E i)) (hG : ∀ i, MeasurableSet (G i)) :
    Summable (fun stage => ∫ θ, sourceSamplingDiagonalContribution stage r b E G θ ∂sourceAngleLaw) := by
…

Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingDiagonalContribution, OAI.FiniteFactor.sourceAngleLaw