OAI/Computability/MaxCut/Games/KMSAnalyticRestrictionTransport.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Coordinate and budget transport for the genuine homogeneous character induction. These statements only change presentations of the actual local squared-density hypothesis and prescribed Fourier sums.

  1. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.mono line 23
  2. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound.codomain_equiv line 29
  3. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_postcomp_injective line 47
  4. def OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv line 79

    Source documentation

    Split off the coordinate measured by a, using the prescribed vector t. The kernel coordinate is exactly x - a x • t.

    def splitEquiv (a : F →ₗ[K] K) (t : F) (ht : a t = 1) :
    F ≃ₗ[K] (a.ker × K) where
…
  5. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_snd line 108
  6. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_fst_coe line 111
  7. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_symm_apply line 114
  8. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_symm_apply_zero line 118
  9. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_ker line 122
  10. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.splitEquiv_apply_unit line 127
  11. theorem OAI.MaxCutGames.Inverse.KMSAnalyticFunctionalSplit.finrank_eq_ker_add_one line 133

    Source documentation

    A functional with a unit preimage has a kernel of codimension one.

    theorem finrank_eq_ker_add_one [FiniteDimensional K F]
    (a : F →ₗ[K] K) (t : F) (ht : a t = 1) :
    Module.finrank K F = Module.finrank K a.ker + 1 := by
…
  12. abbrev OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.F2 line 152
  13. structure OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting line 161

    Source documentation

    Data of one common coordinate and compatible section vectors. All maps and all smaller spaces below are constructed from these original data.

    structure CompatibleSplitting (π : I →ₗ[F2] K) (A : F →ₗ[F2] K) where
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.F2

  14. abbrev OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.K0 line 176
  15. abbrev OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.J line 177
  16. abbrev OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.B line 178
  17. def OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.targetEquiv line 180
  18. def OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftEquiv line 184
  19. def OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightEquiv line 189
  20. def OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap line 195

    Source documentation

    The remaining part of the left surjection is its literal restriction.

    def leftMap (s : CompatibleSplitting π A) : s.J →ₗ[F2] s.K0 :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting, OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.F2

  21. def OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap line 200

    Source documentation

    The remaining part of the right surjection is its literal restriction.

    def rightMap (s : CompatibleSplitting π A) : s.B →ₗ[F2] s.K0 :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting, OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.F2

  22. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap_apply_val line 204
  23. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap_apply_val line 207
  24. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftMap_surjective line 210
  25. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightMap_surjective line 221
  26. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.leftEquiv_symm_apply line 232
  27. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.rightEquiv_symm_apply line 235
  28. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.targetEquiv_symm_apply line 238
  29. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_symm_apply line 241
  30. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_symm_apply line 246
  31. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_conjugation line 252

    Source documentation

    Both changes of coordinates use the same final binary coordinate.

    theorem left_conjugation (s : CompatibleSplitting π A) :
    s.targetEquiv.toLinearMap.comp (π.comp s.leftEquiv.symm.toLinearMap) =
      s.leftMap.prodMap (LinearMap.id : F2 →ₗ[F2] F2) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting, OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.F2

  32. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_conjugation line 260
  33. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.target_finrank line 268
  34. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.left_finrank line 273
  35. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting.right_finrank line 279
  36. theorem OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.exists_compatibleSplitting line 289

    Source documentation

    Positive target dimension supplies a basis coordinate; surjectivity supplies its two lifts. No additional splitting hypothesis is required.

    theorem exists_compatibleSplitting [FiniteDimensional F2 K]
    (π : I →ₗ[F2] K) (A : F →ₗ[F2] K)
    (hπ : Function.Surjective π) (hA : Function.Surjective A)
    (hdim : 0 < Module.finrank F2 K) : Nonempty (CompatibleSplitting π A) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.F2, OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.CompatibleSplitting

  37. def OAI.MaxCutGames.Inverse.KMSAnalyticCompatibleSplitting.chooseSplit line 301
  38. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_bound_induction_inline_KMSAnalyticCharacterInduction line 332
  39. theorem OAI.MaxCutGames.Inverse.KMSAnalytic.fixedFrequencyEnergy_le_of_homogeneous line 407

    Source documentation

    KMS's fixed-character estimate, with actual homogeneous restriction control. The injection is the only ambient-dimension assumption.

    theorem fixedFrequencyEnergy_le_of_homogeneous
    {F : Type v} [AddCommGroup F] [Module F2 F]
    [FiniteDimensional F2 F] [Fintype F]
    {I : Type w} [AddCommGroup I] [Module F2 I]
    [FiniteDimensional F2 I] [Fintype I]
    {J : Type x} [AddCommGroup J] [Module F2 J]
    [FiniteDimensional F2 J] [Fintype J]
    (ι : I →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : IsBasisInvariant f)
    (ε : ℝ) (hg : HomogeneousRestrictionBound (Module.finrank F2 I) ε f)
    (π : I →ₗ[F2] J) (hπ : Function.Surjective π) (A : F →ₗ[F2] J) :
    (2 : ℝ) ^ ((Module.finrank F2 I + Module.finrank F2 J) * Module.finrank F2 E) *
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalytic.HomogeneousRestrictionBound

  40. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_slice_bound line 452

    Source documentation

    KMS's mixed bound with an explicit safe rank-dependent constant. Fixed points and fixed characters are arbitrary; their independence is not assumed.

    theorem mixed_slice_bound (R : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (ι : (A × I) →ₗ[F2] E) (hι : Function.Injective ι)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound (Module.finrank F2 A + Module.finrank F2 I) ε f)
    (a : A →ₗ[F2] F) (π : I →ₗ[F2] J) (hπ : Function.Surjective π)
    (ν : F →ₗ[F2] J) (hr : Module.finrank F2 A + Module.finrank F2 I ≤ R) :
    (2 : ℝ) ^ ((Module.finrank F2 I + Module.finrank F2 J) * Module.finrank F2 E) *
      sliceEnergy (fun T => π.comp T = ν) (partialRestrict (smallComponent ι f) a) ≤
        (2 : ℝ) ^ (4 * R * R) * mixedStepFactor R ^ Module.finrank F2 A * ε := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSFourthMoment.AffineDensityBound, OAI.MaxCutGames.Inverse.KMSFourthMoment.sliceEnergy, OAI.MaxCutGames.Inverse.KMSFourthMoment.partialRestrict, OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor

  41. def OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedRankConstant line 474

    Source documentation

    A single uniform constant for all fixed-point dimensions at rank at most R.

    def mixedRankConstant (R : ℕ) : ℝ := (2 : ℝ) ^ (4 * R * R) * mixedStepFactor R ^ R

    Mentions: OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedStepFactor

  42. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixedRankConstant_nonneg line 476
  43. theorem OAI.MaxCutGames.Inverse.KMSFourthMoment.mixed_slice_bound_uniform line 480
  44. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.mixedMapFintype line 519

    Source documentation

    A consistent finite enumeration of actual binary linear maps, built from the finite vertex spaces. This is the enumeration used by the mixed theorem.

    def mixedMapFintype {V W : Type*}
    [AddCommGroup V] [Module F2 V] [AddCommGroup W] [Module F2 W]
    [Fintype V] [Fintype W] : Fintype (V →ₗ[F2] W) :=
…
  45. def OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound line 534

    Source documentation

    All mixed small-component slices of total degree at most r, with their exact ambient normalization weight. No Hybrid derivative bound is included in this property. Fixed primal points and prescribed frequencies are arbitrary.

    def UniformMixedBound (r : ℕ) (L : ℝ) (f : (E →ₗ[F2] F) → ℝ) : Prop :=
…
  46. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound.pullback line 556

    Source documentation

    Ambient and codomain coordinate pullback preserves every actual mixed slice, while the exponent is unchanged by ambient dimension invariance.

    theorem UniformMixedBound.pullback {r : ℕ} {L : ℝ}
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) (hf : UniformMixedBound r L f) :
    UniformMixedBound r L (fun M => f (LinearEquiv.arrowCongr a b M)) := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound

  47. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound.pullback_iff line 569

    Source documentation

    The uniform mixed property is independent of both ambient coordinate choices. The reverse direction is pullback by the inverse equivalences.

    theorem UniformMixedBound.pullback_iff {r : ℕ} {L : ℝ}
    (a : E ≃ₗ[F2] E') (b : F ≃ₗ[F2] F')
    (f : (E' →ₗ[F2] F') → ℝ) :
    UniformMixedBound r L (fun M => f (LinearEquiv.arrowCongr a b M)) ↔
      UniformMixedBound r L f := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound

  48. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.uniformMixedBound_of_affineDensityBound line 595

    Source documentation

    The proved KMS mixed estimate discharges every instance of the uniform mixed property. Only the actual affine density and basis-invariance hypotheses remain; no Fourier or Hybrid estimate is supplied as a premise.

    theorem uniformMixedBound_of_affineDensityBound (r : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound r ε f) :
    UniformMixedBound r (mixedRankConstant r * ε) f := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound

  49. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.productMixedSliceBound_of_uniform line 634

    Source documentation

    Each image-adapted slice in the product proof is one of the actual uniform mixed slices. The dimension equality exactly matches its weight.

    theorem productMixedSliceBound_of_uniform (i : ℕ) (L : ℝ)
    (f : ((A × U) →ₗ[F2] (B × C)) → ℝ)
    (hMixed : UniformMixedBound i L f)
    (ho : Module.finrank F2 A + Module.finrank F2 C ≤ i)
    (T : (A × U) →ₗ[F2] (B × C)) : ProductMixedSliceBound i f T L := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.ProductMixedSliceBound

  50. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.map_leftRange_complement line 673
  51. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_le_of_uniform line 688

    Source documentation

    The actual hybrid derivative is uniformly bounded whenever all actual mixed slices are bounded. Both selector subspaces and every affine translate are arbitrary.

    theorem hybridDerivative_energy_le_of_uniform
    (i : ℕ) (L : ℝ) (hL : 0 ≤ L)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hMixed : UniformMixedBound i L f) (hi : i ≤ Module.finrank F2 E)
    (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) ≤ L := by
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant, OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.UniformMixedBound

  52. theorem OAI.MaxCutGames.Inverse.KMSAnalyticHybridEnergy.hybridDerivative_energy_bound line 732

    Source documentation

    Genuine KMS hybrid energy bound from basis invariance and actual local squared density. This is the analytic input to the permitted generic fourth moment inequality; no hybrid estimate is included among its hypotheses.

    theorem hybridDerivative_energy_bound
    (i : ℕ) (ε : ℝ) (hε : 0 ≤ ε)
    (f : (E →ₗ[F2] F) → ℝ) (hf : KMSBasisInvariant.IsBasisInvariant f)
    (hd : AffineDensityBound i ε f) (hi : i ≤ Module.finrank F2 E)
    (A : Submodule F2 E) (B : Submodule F2 F) (T : E →ₗ[F2] F) :
    (𝔼 N, hybridDerivative A B T (rankComponent i f) N ^ 2) ≤ mixedRankConstant i * ε :=
…

    Mentions: OAI.MaxCutGames.Inverse.KMSBasisInvariant.IsBasisInvariant