Gaussian.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SubsphereRegression.orthonormal_gaussian_map line 19

Source documentation

Orthonormal coordinates of a standard Gaussian are independent standard normal variables.

lemma orthonormal_gaussian_map {n : ℕ} {u : Fin n → E} (hu : Orthonormal ℝ u) :
    (stdGaussian E).map (fun x => fun i => ⟪u i, x⟫) =
      Measure.pi (fun _ : Fin n => gaussianReal 0 1) := by
…

lemma OAI.SubsphereRegression.gaussianReal_le_volume line 44
lemma OAI.SubsphereRegression.measure_pi_mono line 61
lemma OAI.SubsphereRegression.pi_gaussianReal_le_volume line 74
lemma OAI.SubsphereRegression.gaussian_pairings_le line 77
lemma OAI.SubsphereRegression.measure_pi_smul line 116

lemma OAI.SubsphereRegression.gaussian_rows_pairings_le line 128

Source documentation

Joint domination for an arbitrary number of independent Gaussian rows.

lemma gaussian_rows_pairings_le {n : ℕ} (v : Fin n → E) (hv : LinearIndependent ℝ v)
    (m : ℕ) :
    (Measure.pi (fun _ : Fin m => stdGaussian E)).map
      (fun A => fun j i => ⟪v i, A j⟫) ≤
      ENNReal.ofReal ((∏ i, ‖gramSchmidt ℝ v i‖)⁻¹ ^ m) •
        (volume : Measure (Fin m → Fin n → ℝ)) := by
…

lemma OAI.SubsphereRegression.lintegral_fin_prod line 145
lemma OAI.SubsphereRegression.lintegral_pow_pi line 156

lemma OAI.SubsphereRegression.lintegral_product_differences line 163

Source documentation

Separation of all coordinates in a normalized product mollifier.

lemma lintegral_product_differences (φ : ℝ → ℝ≥0∞) (hφ : Measurable φ)
    (hφ1 : ∫⁻ x, φ x = 1) (m n : ℕ) (y : Fin m → ℝ) :
    ∫⁻ z : Fin m → Fin n → ℝ,
      ∏ j, φ (y j) * ∏ i, φ (y j - z j i) = ∏ j, φ (y j) := by
…

lemma OAI.SubsphereRegression.gaussian_rows_kernel_bound line 183
lemma OAI.SubsphereRegression.gaussian_replica_kernel_bound line 208
def OAI.SubsphereRegression.projectionSmoothing line 245
Source documentation
Product scalar smoothing of the joint matrix--label observation law.
```
def projectionSmoothing (ν : Measure E) (φ : ℝ → ℝ≥0∞) (m : ℕ)
    (z : (Fin m → E) × (Fin m → ℝ)) : ℝ≥0∞ :=
…
```
lemma OAI.SubsphereRegression.measurable_projectionSmoothing line 249
lemma OAI.SubsphereRegression.projectionSmoothing_pow line 255

theorem OAI.SubsphereRegression.projectionSmoothing_moment line 273

Source documentation

Uniform integer moment bound for EVERY normalized nonnegative product mollifier. In particular the constant does not depend on Gaussian noise scale.

theorem projectionSmoothing_moment {ν : Measure E} [IsFiniteMeasure ν]
    {a : ℝ} (hν : HasLocalMassBound ν a)
    (hsupport : ν.support ⊆ Metric.closedBall 0 1)
    (φ : ℝ → ℝ≥0∞) (hφ : Measurable φ) (hφ1 : ∫⁻ z, φ z = 1)
    (m n : ℕ) (hmargin : (n : ℝ) + m ≤ a) :
    ∫⁻ z : (Fin m → E) × (Fin m → ℝ),
      (projectionSmoothing ν φ m z)^(n+1)
      ∂(Measure.pi (fun _ => stdGaussian E)).prod volume ≤
       ν Set.univ * (replicaConstant ν a m)^n := by
…

Mentions: OAI.SubsphereRegression.HasLocalMassBound, OAI.SubsphereRegression.projectionSmoothing, OAI.SubsphereRegression.replicaConstant

lemma OAI.SubsphereRegression.measure_pi_withDensity line 302
lemma OAI.SubsphereRegression.pi_gaussian_map_scale line 329
lemma OAI.SubsphereRegression.pi_gaussian_withDensity line 337
lemma OAI.SubsphereRegression.lintegral_gaussian_shift_scale line 347
lemma OAI.SubsphereRegression.withDensity_apply_le_moment line 374

lemma OAI.SubsphereRegression.map_apply_open_le_of_tendsto line 397

Source documentation

Portmanteau's open-set direction, proved directly from Fatou for this coupling.

lemma map_apply_open_le_of_tendsto (F : X → Y) (Fₖ : ℕ → X → Y)
    (hF : Measurable F) (hFₖ : ∀ k, Measurable (Fₖ k))
    (ht : ∀ x, Tendsto (fun k => Fₖ k x) atTop (𝓝 (F x)))
    (C : ℝ≥0∞) (α : ℝ)
    (hbound : ∀ k U, IsOpen U → (ρ.map (Fₖ k)) U ≤ C * (τ U)^α)
    (U : Set Y) (hU : IsOpen U) :
    (ρ.map F) U ≤ C * (τ U)^α := by
…

lemma OAI.SubsphereRegression.ennreal_rpow_iInf line 436
lemma OAI.SubsphereRegression.measure_apply_le_of_isOpen line 440