PhaseSelection.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Averaging separated selections

Finite probability laws on retained subsets and the scalar weighted phase bound from §9, using the retention cancellation of §8.

structure OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw line 27
Source documentation
Finite probability coordinates and their retained subsets.
```
structure FiniteSelectionLaw where
…
```
def OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.measure line 38
Source documentation
The probability measure represented by the finite coordinates.
```
def measure [MeasurableSpace Ω] (L : FiniteSelectionLaw Ω ι) : Measure Ω :=
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.measure_isProbability line 42
def OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.marginal line 50
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.marginal_nonnegative line 54
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.marginal_le_one line 63
def OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.selectedCoefficient line 71
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.expected_selectedCoefficient line 75
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.expected_selectedFourier line 89
theorem OAI.LipschitzHilbert.PhaseCombinatorics.FiniteSelectionLaw.selected_cost_expectation line 100
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_subset_indicator line 119
theorem OAI.LipschitzHilbert.PhaseCombinatorics.selectedFourier_eq_subtype line 126
theorem OAI.LipschitzHilbert.PhaseCombinatorics.selection_jensen line 136
theorem OAI.LipschitzHilbert.PhaseCombinatorics.retention_cancellation line 145
theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_power_mean line 156
theorem OAI.LipschitzHilbert.PhaseCombinatorics.selected_power_sum_eq_subtype line 193
theorem OAI.LipschitzHilbert.PhaseCombinatorics.lpNorm_finiteFourierSum_eq line 204

theorem OAI.LipschitzHilbert.PhaseCombinatorics.selected_fourier_gain line 215

Source documentation

Averaging inverse-marginal reconstructions costs exactly the expected ℓ^r coefficient mass. All Fourier estimates here are already proved.

theorem selected_fourier_gain (L : FiniteSelectionLaw Ω ι)
    (ν : Measure ℝ) [IsProbabilityMeasure ν] (frequency : ι → ℝ) (a : ι → ℂ)
    {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 ω → Separated (fun i : L.retained ω => frequency i) gap)
    (hcard : ∀ ω, 0 < L.weight ω → ((L.retained ω).card : ℝ) ≤ D)
    (hr : 1 ≤ fourierInterpolationExponent D p) :
    (∫ t, ‖finiteFourierSum 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.finiteFourierSum

theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_coefficient_cost line 271

theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_phase_bound line 305

Source documentation

The scalar inequality pred:weighted-phase-bound for a finite selection law with the stated separation and marginal guarantees.

theorem weighted_phase_bound (L : FiniteSelectionLaw Ω ι)
    (ν : Measure ℝ) [IsProbabilityMeasure ν] (frequency : ι → ℝ)
    (l q : ι → ℝ) (X lambda : ι → ℂ) {gap D p μ : ℝ}
    (hgap : 0 < gap) (hν : FourierGap ν gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hsep : ∀ ω, 0 < L.weight ω → Separated (fun i : L.retained ω => frequency i) 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 ^ μ)
    (hr : 1 ≤ fourierInterpolationExponent D p)
    (hrp : fourierInterpolationExponent D p ≤ p)
    (hμr : μ * fourierInterpolationExponent D p = fourierInterpolationExponent D p - 1) :
…

theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_prediction_average line 330

Source documentation

Add the mass baseline and divide by its constant denominator.

theorem weighted_prediction_average (L : FiniteSelectionLaw Ω ι)
    (ν : Measure ℝ) [IsProbabilityMeasure ν] (frequency : ι → ℝ)
    (l q : ι → ℝ) (X lambda : ι → ℂ) {gap D p μ : ℝ}
    (hgap : 0 < gap) (hν : FourierGap ν gap) (hD : 1 ≤ D) (hp : 4 ≤ p)
    (hsep : ∀ ω, 0 < L.weight ω → Separated (fun i : L.retained ω => frequency i) 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 ^ μ)
    (hr : 1 ≤ fourierInterpolationExponent D p)
    (hrp : fourierInterpolationExponent D p ≤ p)
    (hμr : μ * fourierInterpolationExponent D p = fourierInterpolationExponent D p - 1) :
…

def OAI.LipschitzHilbert.PhaseCombinatorics.phaseMu line 362
theorem OAI.LipschitzHilbert.PhaseCombinatorics.phase_selection_parameters line 365
theorem OAI.LipschitzHilbert.PhaseCombinatorics.weighted_prediction_average_at_p line 388