OAI/Analysis/ModularTheory/GaussianRegularizers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Concrete Gaussian regularizers in the modular core. Their square weight is finite and they converge strongly to the identity. No trace identity is assumed in this construction.

  1. def OAI.WeakPureInfiniteness.modularGaussian line 16
  2. lemma OAI.WeakPureInfiniteness.modularGaussian_apply line 24
  3. lemma OAI.WeakPureInfiniteness.modularGaussian_norm_le line 27
  4. lemma OAI.WeakPureInfiniteness.modularGaussian_tendsto line 33
  5. lemma OAI.WeakPureInfiniteness.modularGaussian_integrable line 42
  6. def OAI.WeakPureInfiniteness.modularGaussianRegularizer line 65
  7. lemma OAI.WeakPureInfiniteness.modularGaussianRegularizer_mem line 69
  8. lemma OAI.WeakPureInfiniteness.modularGaussianRegularizer_finite line 73
  9. lemma OAI.WeakPureInfiniteness.modularGaussianRegularizer_strong line 78
  10. theorem OAI.WeakPureInfiniteness.modularCore_finiteWeight_approximation line 99

    Source documentation

    The finite-square-weight left ideal is strongly dense in the actual core. This is a semifiniteness step, separate from tracial symmetry.

    theorem modularCore_finiteWeight_approximation
    (T : Lp H 2 (volume : Measure ℝ) →L[ℂ] Lp H 2 (volume : Measure ℝ))
    (hT : T ∈ modularCrossedProduct (volume : Measure ℝ) S) :
    ∃ R : ℕ → (Lp H 2 (volume : Measure ℝ) →L[ℂ] Lp H 2 (volume : Measure ℝ)),
      (∀ n, R n ∈ modularCrossedProduct (volume : Measure ℝ) S) ∧
      (∀ n, modularCoreSquareWeight S (R n) < ⊤) ∧
      ∀ f, Tendsto (fun n => R n f) atTop (𝓝 (T f)) := by
…

    Mentions: OAI.WeakPureInfiniteness.modularCrossedProduct, OAI.WeakPureInfiniteness.modularCoreSquareWeight