FiberProjection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Correlation over paired finite fibers

The component totals determine equal-cardinality fibers. Cauchy--Schwarz on their sums, together with invariance under a cycle action, gives the finite projection reduction before the local quartet bounds are applied.

def OAI.Ostmann.fiberSum line 17
theorem OAI.Ostmann.complex_correlation_sq_le line 21

theorem OAI.Ostmann.fiberSum_energy_le line 33

Source documentation

A common fiber-size bound controls the energy of the fiber sums.

theorem fiberSum_energy_le {Ω T : Type*} [Fintype Ω] [Fintype T] [DecidableEq T]
    (τ : Ω → T) (f : Ω → ℂ) (N : ℕ)
    (hN : ∀ t, (Finset.univ.filter (fun x => τ x = t)).card ≤ N) :
    (∑ t : T, ‖fiberSum τ f t‖ ^ 2) ≤ (N : ℝ) * ∑ x : Ω, ‖f x‖ ^ 2 := by
…

Mentions: OAI.Ostmann.fiberSum

theorem OAI.Ostmann.fiberSum_actionAverage line 55

Source documentation

A fiber-preserving finite action does not change the fiber sums.

theorem fiberSum_actionAverage {G Ω T : Type*} [Group G] [Fintype G]
    [Fintype Ω] [DecidableEq T] [MulAction G Ω]
    (τ : Ω → T) (hτ : ∀ (g : G) x, τ (g • x) = τ x) (f : Ω → ℂ) (t : T) :
    fiberSum τ (finiteActionAverage (G := G) f) t = fiberSum τ f t := by
…

Mentions: OAI.Ostmann.fiberSum, OAI.Ostmann.finiteActionAverage

theorem OAI.Ostmann.pairedFiber_correlation_sq_le line 65

Source documentation

The squared projection reduction; normalization can be applied afterward.

theorem pairedFiber_correlation_sq_le {G Ω T : Type*} [Group G] [Fintype G]
    [Fintype Ω] [Fintype T] [DecidableEq T] [MulAction G Ω]
    (τ : Ω → T) (hτ : ∀ (g : G) x, τ (g • x) = τ x)
    (f g : Ω → ℂ) (N : ℕ)
    (hN : ∀ t, (Finset.univ.filter (fun x => τ x = t)).card ≤ N) :
    ‖∑ t : T, fiberSum τ f t * conj (fiberSum τ g t)‖ ^ 2 ≤
      (N : ℝ) ^ 2 * (∑ x : Ω, ‖finiteActionAverage (G := G) f x‖ ^ 2) *
…

Mentions: OAI.Ostmann.fiberSum, OAI.Ostmann.finiteActionAverage

theorem OAI.Ostmann.pairedFiber_correlation_eq line 84

Source documentation

Expanding the two fiber sums gives the equal-total paired correlation.

theorem pairedFiber_correlation_eq {Ω T : Type*} [Fintype Ω] [Fintype T] [DecidableEq T]
    (τ : Ω → T) (f g : Ω → ℂ) :
    (∑ t : T, fiberSum τ f t * conj (fiberSum τ g t)) =
      ∑ x : Ω, ∑ y : Ω, if τ x = τ y then f x * conj (g y) else 0 := by
…

Mentions: OAI.Ostmann.fiberSum

theorem OAI.Ostmann.pairedFiber_normalized_projection line 102

Source documentation

Probability-normalized form of the finite cycle projection reduction.

theorem pairedFiber_normalized_projection {G Ω T : Type*} [Group G] [Fintype G]
    [Fintype Ω] [Nonempty Ω] [Fintype T] [DecidableEq T] [MulAction G Ω]
    (τ : Ω → T) (hτ : ∀ (g : G) x, τ (g • x) = τ x)
    (f g : Ω → ℂ) (N : ℕ) (hNpos : 0 < N)
    (hN : ∀ t, (Finset.univ.filter (fun x => τ x = t)).card ≤ N) :
    ‖((Fintype.card Ω : ℂ) * (N : ℂ))⁻¹ *
      (∑ x : Ω, ∑ y : Ω, if τ x = τ y then f x * conj (g y) else 0)‖ ^ 2 ≤
      ((∑ x : Ω, ‖finiteActionAverage (G := G) f x‖ ^ 2) / (Fintype.card Ω : ℝ)) *
…

Mentions: OAI.Ostmann.finiteActionAverage