DiagonalPhaseSelection.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Averaging diagonal Hilbert-valued phases

The weighted prediction bound of §9 for finite-dimensional Hilbert vectors and coordinate-dependent frequencies. The retained-set estimate is the proved constant-one diagonal Fourier gain; the marginal cancellation is exact.

theorem OAI.LipschitzHilbert.PhaseCombinatorics.euclidean_sum_apply line 27
theorem OAI.LipschitzHilbert.PhaseCombinatorics.euclidean_norm_rpow line 35
def OAI.LipschitzHilbert.PhaseCombinatorics.diagonalModulation line 44
Source documentation
Coordinatewise modulation by unit characters.
```
def diagonalModulation (frequency : κ → ℝ) (a : EuclideanSpace ℂ κ) (t : ℝ) :
    EuclideanSpace ℂ κ := WithLp.toLp 2 (fun j => a j * character (frequency j) t)
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.character
theorem OAI.LipschitzHilbert.PhaseCombinatorics.norm_diagonalModulation line 48
def OAI.LipschitzHilbert.PhaseCombinatorics.diagonalFourierSum line 55
Source documentation
A diagonal phase sum, represented in the actual Euclidean Hilbert norm.
```
def diagonalFourierSum (frequency : ι → κ → ℝ) (a : ι → EuclideanSpace ℂ κ)
    (t : ℝ) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.PhaseCombinatorics.diagonalFourierSum_eq_sum line 60
theorem OAI.LipschitzHilbert.PhaseCombinatorics.continuous_diagonalFourierSum line 69
theorem OAI.LipschitzHilbert.PhaseCombinatorics.diagonalFourierSum_bound line 75
theorem OAI.LipschitzHilbert.PhaseCombinatorics.lpNorm_diagonalFourierSum_eq line 83
theorem OAI.LipschitzHilbert.PhaseCombinatorics.diagonal_fourier_gain_norm line 93
def OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.selectedVector line 106
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.selectedVector_apply line 111
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.norm_selectedVector line 118
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.expected_selectedDiagonal line 127
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.selected_vector_cost line 139
theorem OAI.LipschitzHilbert.PhaseCombinatorics.selectedDiagonal_eq_subtype line 156
theorem OAI.LipschitzHilbert.PhaseCombinatorics.selected_vector_power_sum_eq_subtype line 167

theorem OAI.LipschitzHilbert.PhaseCombinatorics.selected_diagonal_fourier_gain line 179

Source documentation

Inverse-marginal averaging of diagonal Hilbert phases.

theorem selected_diagonal_fourier_gain (L : FiniteSelectionLaw Ω ι)
    (ν : Measure ℝ) [IsProbabilityMeasure ν] (frequency : ι → κ → ℝ)
    (a : ι → EuclideanSpace ℂ κ) {gap D p : ℝ}
    (hgap : 0 < gap) (hν : FourierGap ν gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hπ : ∀ i, 0 < L.marginal i)
    (hsep : ∀ ω, 0 < L.weight ω → ∀ j,
      Separated (fun i : L.retained ω => frequency i j) gap)
    (hcard : ∀ ω, 0 < L.weight ω → ((L.retained ω).card : ℝ) ≤ D)
    (hr : 1 ≤ fourierInterpolationExponent D p) :
    (∫ t, ‖diagonalFourierSum frequency a t‖ ^ p ∂ν) ^ (1 / p) ≤
      (∑ i, L.marginal i * (‖a i‖ / L.marginal i) ^ fourierInterpolationExponent D p) ^
        (1 / fourierInterpolationExponent D p) := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap, OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.fourierInterpolationExponent, OAI.LipschitzHilbert.PhaseCombinatorics.diagonalFourierSum

theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_vector_coefficient_cost line 238

Source documentation

The scalar marginal cancellation applies to Hilbert vectors through their norms.

theorem weighted_vector_coefficient_cost (l : ι → ℝ) (X : ι → EuclideanSpace ℂ κ)
    (lambda : ι → ℂ) (π q : ι → ℝ) {μ r : ℝ}
    (hl : ∀ i, 0 ≤ l i) (hπ : ∀ i, 0 < π i) (hq : ∀ i, 0 < q i)
    (hqπ : ∀ i, q i ≤ π i) (hlambda : ∀ i, ‖lambda i‖ ≤ q i ^ μ)
    (hr : 1 ≤ r) (hμr : μ * r = r - 1) :
    (∑ i, π i * (‖(((l i ^ (1 - μ) : ℝ) : ℂ) * lambda i) • X i‖ / π i) ^ r) ≤
      ∑ i, l i * ‖X i‖ ^ r := by
…

theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_diagonal_phase_bound line 249

theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_diagonal_prediction_average_at_p line 276

Source documentation

The full finite-dimensional diagonal weighted prediction average of §9.

theorem weighted_diagonal_prediction_average_at_p (L : FiniteSelectionLaw Ω ι)
    (ν : Measure ℝ) [IsProbabilityMeasure ν] (frequency : ι → κ → ℝ)
    (l q : ι → ℝ) (X : ι → EuclideanSpace ℂ κ) (lambda : ι → ℂ)
    {gap D p : ℝ} (hgap : 0 < gap) (hν : FourierGap ν gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hsep : ∀ ω, 0 < L.weight ω → ∀ j,
      Separated (fun i : L.retained ω => frequency i j) gap)
    (hcard : ∀ ω, 0 < L.weight ω → ((L.retained ω).card : ℝ) ≤ D)
    (hl : ∀ i, 0 ≤ l i) (htotal : ∑ i, l i ≤ 1)
    (hq : ∀ i, 0 < q i) (hqπ : ∀ i, q i ≤ L.marginal i)
    (hlambda : ∀ i, ‖lambda i‖ ≤ q i ^ phaseMu D p) :
    (∫ t, (1 + ‖diagonalFourierSum frequency
      (fun i => (((l i ^ (1 - phaseMu D p) : ℝ) : ℂ) * lambda i) • X i) t‖ ^ p) /
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw, OAI.LipschitzHilbert.PhaseCombinatorics.FourierGap, OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.phaseMu, OAI.LipschitzHilbert.PhaseCombinatorics.diagonalFourierSum