KMSAnalyticHybridEnergySupport.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact rank support of actual hybrid derivatives

The actual Hybrid selector loses exactly dim A + codim B in rank. Consequently a pure rank component has derivative coefficients supported at that exact remaining rank. Orders above the original rank give zero.

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybrid_frequency_rank line 35

Source documentation

The actual selector implies the exact rank loss for the actual compressed Fourier frequency.

theorem hybrid_frequency_rank (A : Submodule F2 E) (B : Submodule F2 F)
    (S : F →ₗ[F2] E) (hS : LinearIdentities.Hybrid S A B) :
    Module.finrank F2 (Restriction.compressFrequency A B S).range + order A B =
      Module.finrank F2 S.range := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.linearCoeff_hybridDerivative_rankComponent_eq_zero line 51

Source documentation

A rank-i component has no derivative coefficient away from the exact compressed rank plus the order.

theorem linearCoeff_hybridDerivative_rankComponent_eq_zero
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ)
    (Z : B →ₗ[F2] (E ⧸ A))
    (hZ : Module.finrank F2 Z.range + order A B ≠ i) :
    linearCoeff (hybridDerivative A B T (rankComponent i f)) Z = 0 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_eq_zero_of_lt_order line 72

Source documentation

If the order is larger than the selected rank, the actual derivative vanishes, including all affine translates.

theorem hybridDerivative_rankComponent_eq_zero_of_lt_order
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ)
    (hi : i < order A B) :
    hybridDerivative A B T (rankComponent i f) = 0 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_support line 84

Source documentation

Parseval restricted to the exact rank-loss equality.

theorem hybridDerivative_rankComponent_energy_eq_support
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A) with Module.finrank F2 Z.range + order A B = i,
        linearCoeff (hybridDerivative A B T (rankComponent i f)) Z ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_rank line 102

Source documentation

Exact normalized energy is supported on compressed frequencies of rank i - order A B. This also holds above the order cutoff since every coefficient then vanishes.

theorem hybridDerivative_rankComponent_energy_eq_rank
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A) with Module.finrank F2 Z.range = i - order A B,
        linearCoeff (hybridDerivative A B T (rankComponent i f)) Z ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_energy_eq_rank_fibers line 120

Source documentation

The rank-restricted exact energy written in the actual compressed Fourier fibers used by the analytic estimate.

theorem hybridDerivative_rankComponent_energy_eq_rank_fibers
    (A : Submodule F2 E) (B : Submodule F2 F)
    [Fintype (B →ₗ[F2] (E ⧸ A))]
    (T : E →ₗ[F2] F) (f : (E →ₗ[F2] F) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] (E ⧸ A) with Module.finrank F2 Z.range = i - order A B,
        (∑ S : F →ₗ[F2] E,
          if LinearIdentities.Hybrid S A B ∧ Restriction.compressFrequency A B S = Z
          then linearCoeff (rankComponent i f) S * (linearTraceCharacter S T).re
          else 0) ^ 2 := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv_finrank line 144
Source documentation
The explicit change from quotient frequencies to blocks preserves rank.
```
theorem productFrequencyEquiv_finrank
    (Z : (LinearMap.range (LinearMap.inl F2 B C)) →ₗ[F2]
      ((A × U) ⧸ LinearMap.range (LinearMap.inl F2 A U))) :
    Module.finrank F2 (productFrequencyEquiv Z).range = Module.finrank F2 Z.range := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.productFrequencyEquiv

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.product_restriction_order line 157

Source documentation

The intrinsic restriction order agrees with the two fixed block dimensions.

theorem product_restriction_order :
    order (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) =
      Module.finrank F2 A + Module.finrank F2 C := by
…

theorem OAI.UniqueGamesTheorem.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_rankComponent_product_energy_eq_rank_fibers line 170

Source documentation

The actual derivative energy, restricted to the exact ordinary block rank.

theorem hybridDerivative_rankComponent_product_energy_eq_rank_fibers
    (T : (A × U) →ₗ[F2] (B × C))
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ) (i : ℕ) :
    (𝔼 N, hybridDerivative (LinearMap.range (LinearMap.inl F2 A U))
      (LinearMap.range (LinearMap.inl F2 B C)) T (rankComponent i f) N ^ 2) =
      ∑ Z : B →ₗ[F2] U with
          Module.finrank F2 Z.range = i - (Module.finrank F2 A + Module.finrank F2 C),
        (∑ S : (B × C) →ₗ[F2] (A × U),
          if LinearIdentities.Hybrid S (LinearMap.range (LinearMap.inl F2 A U))
              (LinearMap.range (LinearMap.inl F2 B C)) ∧
              (LinearMap.snd F2 A U).comp (S.comp (LinearMap.inl F2 B C)) = Z
          then linearCoeff (rankComponent i f) S * (linearTraceCharacter S T).re
…