MovingDiagonalEnergy.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The original diagonal with its common transform and original prior

theorem OAI.Ostmann.finite_diagonal_common_transform line 13

Source documentation

Only the finitely many attained keys are used; products and frequencies need not have finite ambient types.

theorem finite_diagonal_common_transform {A K : Type*} [Fintype A] [DecidableEq K]
    (key : A → K) (W : A → ℂ) (G : K → ℂ) :
    (∑ a, ∑ b, if key a = key b then
      (W a * G (key a)) * conj (W b * G (key b)) else 0).re =
      ∑ k ∈ Finset.univ.image key, ‖G k‖ ^ 2 * ‖groupedCoefficient key W k‖ ^ 2 := by
…

Mentions: OAI.Ostmann.groupedCoefficient

theorem OAI.Ostmann.moving_regular_pivot_diagonal line 35

Source documentation

The actual regular diagonal groups every ordered arrangement on the same product/frequency fibre before taking its squared modulus.

theorem moving_regular_pivot_diagonal {A H : Type*} [Fintype A] [Fintype H]
    (p : A → H → ℕ) [∀ a i, Fact (p a i).Prime]
    (g : ∀ q : ℕ, ZMod q → ℂ) (M : ℕ) (v : A → ℤ) (W : A → ℂ)
    (hinj : ∀ a, W a ≠ 0 → Function.Injective (p a))
    (hv : ∀ a, W a ≠ 0 → v a ≠ 0)
    (hsmall : ∀ a, W a ≠ 0 → ∀ i, (v a).natAbs < p a i) :
    (pivotDiagonal (fun a => ∏ i, p a i) v
      (fun a => W a * movingRegularTransform (p a) (fun i => g (p a i)) M (v a))).re =
      ∑ k ∈ Finset.univ.image (fun a => ((∏ i, p a i), v a)),
        ‖primeProductTransform g M k.1 k.2‖ ^ 2 *
          ‖groupedCoefficient (fun a => ((∏ i, p a i), v a)) W k‖ ^ 2 := by
…

Mentions: OAI.Ostmann.pivotDiagonal, OAI.Ostmann.movingRegularTransform, OAI.Ostmann.primeProductTransform, OAI.Ostmann.groupedCoefficient

theorem OAI.Ostmann.grouped_weighted_norm_sq_le line 79

Source documentation

Cauchy on one fibre retains its original prior and charges the other branch only through that fibre's original mass.

theorem grouped_weighted_norm_sq_le {A K : Type*} [Fintype A]
    (key : A → K) (μ : A → ℝ) (W : A → ℂ) (k : K) (θ : ℝ)
    (hμ : ∀ a, 0 ≤ μ a)
    (hmass : (∑ a, if key a = k then μ a else 0) ≤ θ) :
    ‖groupedCoefficient key (fun a => (μ a : ℂ) * W a) k‖ ^ 2 ≤
      θ * ∑ a, if key a = k then μ a * ‖W a‖ ^ 2 else 0 := by
…

Mentions: OAI.Ostmann.groupedCoefficient

theorem OAI.Ostmann.weighted_diagonal_common_transform_le line 100

Source documentation

The diagonal energy after grouping, suitable for the prior atom bound and the subsequent regular-prime cancellation.

theorem weighted_diagonal_common_transform_le {A K : Type*} [Fintype A] [Fintype K]
    (key : A → K) (μ : A → ℝ) (W : A → ℂ) (G : K → ℂ) (θ : K → ℝ)
    (hμ : ∀ a, 0 ≤ μ a)
    (hmass : ∀ k, (∑ a, if key a = k then μ a else 0) ≤ θ k) :
    (∑ a, ∑ b, if key a = key b then
      ((μ a : ℂ) * W a * G (key a)) * conj ((μ b : ℂ) * W b * G (key b)) else 0).re ≤
      ∑ a, μ a * θ (key a) * ‖W a * G (key a)‖ ^ 2 := by
…

theorem OAI.Ostmann.finite_weighted_diagonal_common_transform_le line 128

Source documentation

The same fibre estimate for unbounded integer product/frequency keys. Only the finite image of the sample space is introduced as a finite type.

theorem finite_weighted_diagonal_common_transform_le {A K : Type*}
    [Fintype A] [DecidableEq K]
    (key : A → K) (μ : A → ℝ) (W : A → ℂ) (G : K → ℂ) (θ : K → ℝ)
    (hμ : ∀ a, 0 ≤ μ a)
    (hmass : ∀ k, (∑ a, if key a = k then μ a else 0) ≤ θ k) :
    (∑ a, ∑ b, if key a = key b then
      ((μ a : ℂ) * W a * G (key a)) * conj ((μ b : ℂ) * W b * G (key b)) else 0).re ≤
      ∑ a, μ a * θ (key a) * ‖W a * G (key a)‖ ^ 2 := by
…

theorem OAI.Ostmann.finite_grouped_weighted_energy_le line 143

theorem OAI.Ostmann.moving_regular_pivot_diagonal_le line 156

Source documentation

The actual giant-transfer diagonal is bounded using one original prior and one matching-fibre mass, with no frequency-count loss.

theorem moving_regular_pivot_diagonal_le {A H : Type*} [Fintype A] [Fintype H]
    (p : A → H → ℕ) [∀ a i, Fact (p a i).Prime]
    (g : ∀ q : ℕ, ZMod q → ℂ) (M : ℕ) (v : A → ℤ)
    (μ : A → ℝ) (W : A → ℂ) (θ : ℕ × ℤ → ℝ)
    (hμ : ∀ a, 0 ≤ μ a)
    (hinj : ∀ a, (μ a : ℂ) * W a ≠ 0 → Function.Injective (p a))
    (hv : ∀ a, (μ a : ℂ) * W a ≠ 0 → v a ≠ 0)
    (hsmall : ∀ a, (μ a : ℂ) * W a ≠ 0 → ∀ i, (v a).natAbs < p a i)
    (hmass : ∀ k, (∑ a, if ((∏ i, p a i), v a) = k then μ a else 0) ≤ θ k) :
    (pivotDiagonal (fun a => ∏ i, p a i) v
      (fun a => (μ a : ℂ) * W a *
        movingRegularTransform (p a) (fun i => g (p a i)) M (v a))).re ≤
…

Mentions: OAI.Ostmann.pivotDiagonal, OAI.Ostmann.movingRegularTransform