D.4 Why the spectral measure cannot be dilated🔗

PropositionD.3

Statement uses 2

Statement dependency previews

Preview

Definition Aux.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Let \dim H=\infty and let W be injective, positive, self-adjoint, and trace class with eigenvectors e_j and eigenvalues w_j>0. The sets E_t, t>0, are Borel (i a) and pairwise disjoint (i b), \mathcal N(0,tW)(E_t)=1 (i c), and consequently a \sigma-finite measure dominates \mathcal N(0,tW) for at most countably many t (i d). Hence, for a bounded Borel r with \{r\ne0\} of positive measure, there is no finite complex Borel measure \Gamma on H\times\mathbb R whose bias slices satisfy \int_{E\times\mathbb R}e^{i\omega c}\,\Gamma(\mathrm da,\mathrm dc)=r(\omega)(D_{1/\omega})_\#\mathcal N(0,W)(E) for almost every \omega\ne0 (ii).

Lean code for PropositionD.3●5 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_D_3_i_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j) (t : ℝ) :
  MeasurableSet (OperatorRidgelet.strongLawSet (⇑e) w t)

theorem OperatorRidgelet.Paper.prop_D_3_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (t : ℝ) :
  MeasurableSet
    (OperatorRidgelet.strongLawSet (⇑e) w
      t)

**Proposition [prop:D.3]** Dilation obstruction.  The sets `E_t` are Borel.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_D_3_i_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j) (t t' : ℝ) :
  t ≠ t' →
    Disjoint (OperatorRidgelet.strongLawSet (⇑e) w t)
      (OperatorRidgelet.strongLawSet (⇑e) w t')

theorem OperatorRidgelet.Paper.prop_D_3_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (t t' : ℝ) :
  t ≠ t' →
    Disjoint
      (OperatorRidgelet.strongLawSet (⇑e)
        w t)
      (OperatorRidgelet.strongLawSet (⇑e)
        w t')

**Proposition [prop:D.3]** Dilation obstruction.  The sets `E_t` are pairwise
disjoint.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_D_3_i_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t → OperatorRidgelet.IsCenteredGaussian (t • W) (γ t))
  (t : ℝ) : 0 < t → (γ t) (OperatorRidgelet.strongLawSet (⇑e) w t) = 1

theorem OperatorRidgelet.Paper.prop_D_3_i_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t →
        OperatorRidgelet.IsCenteredGaussian
          (t • W) (γ t))
  (t : ℝ) :
  0 < t →
    (γ t)
        (OperatorRidgelet.strongLawSet
          (⇑e) w t) =
      1

**Proposition [prop:D.3]** Dilation obstruction.  For `t > 0`,
`𝒩(0,tW)(E_t) = 1`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_D_3_i_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t → OperatorRidgelet.IsCenteredGaussian (t • W) (γ t))
  (ν : MeasureTheory.Measure H) :
  MeasureTheory.SigmaFinite ν →
    {t | 0 < t ∧ (γ t).AbsolutelyContinuous ν}.Countable

theorem OperatorRidgelet.Paper.prop_D_3_i_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γ : ℝ → MeasureTheory.Measure H)
  (hγ :
    ∀ (t : ℝ),
      0 < t →
        OperatorRidgelet.IsCenteredGaussian
          (t • W) (γ t))
  (ν : MeasureTheory.Measure H) :
  MeasureTheory.SigmaFinite ν →
    {t |
        0 < t ∧
          (γ t).AbsolutelyContinuous
            ν}.Countable

**Proposition [prop:D.3]** Dilation obstruction.  Consequently a σ-finite
measure dominates `𝒩(0,tW)` for at most countably many `t > 0`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.prop_D_3_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {W : H →L[ℝ] H}
  (hW : OperatorRidgelet.IsTraceClassCovariance W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j) (γW : MeasureTheory.Measure H)
  (hγW : OperatorRidgelet.IsCenteredGaussian W γW) (r : ℝ → ℝ)
  (hr : Measurable r) (hrb : ∃ M, ∀ (ω : ℝ), |r ω| ≤ M)
  (hr0 : 0 < MeasureTheory.volume {ω | r ω ≠ 0}) :
  ¬∃ m,
      MeasureTheory.IsFiniteMeasure m ∧
        ∃ h,
          MeasureTheory.Integrable h m ∧
            ∀ᵐ (ω : ℝ),
              ω ≠ 0 →
                ∀ (E : Set H),
                  MeasurableSet E →
                    ∫ (q : H × ℝ) in E ×ˢ Set.univ,
                        Complex.exp (↑(ω * q.2) * Complex.I) * h q ∂m =
                      ↑(r ω) *
                        ↑((MeasureTheory.Measure.map (fun a => ω⁻¹ • a)
                                γW)
                              E).toReal

theorem OperatorRidgelet.Paper.prop_D_3_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {W : H →L[ℝ] H}
  (hW :
    OperatorRidgelet.IsTraceClassCovariance
      W)
  (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ)
  (hw : ∀ (j : ℕ), 0 < w j)
  (hWe : ∀ (j : ℕ), W (e j) = w j • e j)
  (γW : MeasureTheory.Measure H)
  (hγW :
    OperatorRidgelet.IsCenteredGaussian W
      γW)
  (r : ℝ → ℝ) (hr : Measurable r)
  (hrb : ∃ M, ∀ (ω : ℝ), |r ω| ≤ M)
  (hr0 :
    0 <
      MeasureTheory.volume
        {ω | r ω ≠ 0}) :
  ¬∃ m,
      MeasureTheory.IsFiniteMeasure m ∧
        ∃ h,
          MeasureTheory.Integrable h m ∧
            ∀ᵐ (ω : ℝ),
              ω ≠ 0 →
                ∀ (E : Set H),
                  MeasurableSet E →
                    ∫ (q : H × ℝ) in
                        E ×ˢ Set.univ,
                        Complex.exp
                            (↑(ω * q.2) *
                              Complex.I) *
                          h q ∂m =
                      ↑(r ω) *
                        ↑((MeasureTheory.Measure.map
                                (fun a =>
                                  ω⁻¹ • a)
                                γW)
                              E).toReal

**Proposition [prop:D.3]** Dilation obstruction.  For a bounded Borel `r`
with `{r ≠ 0}` of positive Lebesgue measure, no finite complex Borel measure `Γ = h m` on
`H × ℝ` (a finite measure `m` with an integrable density `h`) has bias slices
`Γ⁺_ω(E) = ∫_{E×ℝ} e^{iωc} Γ(da,dc) = r(ω) (D_{1/ω})_# 𝒩(0,W)(E)` for almost every `ω ≠ 0`.

Proof for Proposition D.3

uses 0

The strong law of large numbers for the independent normalized Gaussian coordinates gives \mathcal N(0,tW)(E_t)=1, a \sigma-finite measure has at most countably many disjoint sets of positive measure, and a measure \Gamma as in (ii) would give a finite measure dominating \mathcal N(0,W/\omega^2) for uncountably many \omega.