FixedPathAverage.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform averages of the actual graph prediction

The band-limited probability is an explicit mixture. Its graph-prediction average is at most one by the proved phase gain. Removing the path carrier then bounds the lower deviation by the off-path coefficient mass, preserving the relative path drop when passing to the principal probability.

def OAI.LipschitzHilbert.predictionMixture line 29
Source documentation
The actual probability mixture used to approximate cell averages.
```
def predictionMixture (ω τ : Measure ℝ) (η : ℝ) : Measure ℝ :=
…
```
theorem OAI.LipschitzHilbert.predictionMixture_isProbability line 33
theorem OAI.LipschitzHilbert.integrable_diagonal_energyRatio line 42

theorem OAI.LipschitzHilbert.diagonal_prediction_mixture_transfer line 55

Source documentation

Uniform-average transfer for the actual diagonal phase sum, with the constant denominator canceled through exact carrier removal.

theorem diagonal_prediction_mixture_transfer (ω τ : Measure ℝ)
    [IsProbabilityMeasure ω] [IsProbabilityMeasure τ]
    (frequency : ι → κ → ℝ) (a : ι → EuclideanSpace ℂ κ) (i₀ : ι)
    {η p denominator B : ℝ} (hη0 : 0 ≤ η) (hη1 : η < 1)
    (hp : 1 ≤ p) (hd : 0 < denominator) (hB : 0 ≤ B)
    (hmass : (∑ i : RemainderIndex i₀, ‖a i‖) ≤ B)
    (haverage : (∫ t, energyRatio p denominator (diagonalFourierSum frequency a t)
      ∂predictionMixture ω τ η) ≤ 1) :
    (∫ t, energyRatio p denominator (diagonalFourierSum frequency a t) ∂ω) ≤
      1 + η / (1 - η) * (2 * p * B) := by
…

Mentions: OAI.LipschitzHilbert.energyRatio, OAI.LipschitzHilbert.predictionMixture

theorem OAI.LipschitzHilbert.graph_prediction_uniform_average line 86

Source documentation

The full graph-prediction average on the principal probability, after paying only the off-path mass in the probability-mixture error.

theorem graph_prediction_uniform_average
    (G : ι → ι → Prop) (hG : ∀ ⦃i j⦄, G i j → G j i)
    (w m : ι → ℝ) (hw : ∀ i, 0 < w i)
    (hm : ∀ i, orderMass w (closedNeighborhood G i) ≤ m i)
    (ω τ : Measure ℝ) [IsProbabilityMeasure ω] [IsProbabilityMeasure τ]
    (frequency : ι → κ → ℝ) (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
    (lambda : ι → ℂ) (i₀ : ι) {η gap D p B : ℝ}
    (hη0 : 0 ≤ η) (hη1 : η < 1) (hgap : 0 < gap)
    (hν : FourierGap (predictionMixture ω τ η) gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hfrequency : ∀ i j, i ≠ j → ¬G i j → ∀ k, gap ≤ |frequency i k - frequency j k|)
    (hcard : ∀ S : Finset ι, (S : Set ι).Pairwise (fun i j => ¬G i j) → (S.card : ℝ) ≤ D)
    (hl : ∀ i, 0 ≤ l i) (htotal : ∑ i, l i ≤ 1)
…

Mentions: OAI.LipschitzHilbert.orderMass, OAI.LipschitzHilbert.closedNeighborhood, OAI.LipschitzHilbert.predictionMixture