Orbits.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SidorenkoCounterexample.card_le_card_mul_of_fibers line 10

Source documentation

Counting a finite set by uniformly bounded fibers.

theorem card_le_card_mul_of_fibers {A B : Type*} [Finite A] [Finite B]
    (f : A → B) (m : ℕ) (h : ∀ b, Nat.card {a : A // f a = b} ≤ m) :
    Nat.card A ≤ Nat.card B * m := by
…

theorem OAI.SidorenkoCounterexample.square_fiber_card line 29
Source documentation
A quadratic equation with no linear term has at most two roots.
```
theorem square_fiber_card (a : K) : Nat.card {x : K // x^2 = a} ≤ 2 := by
…
```
theorem OAI.SidorenkoCounterexample.norm_sphere_count line 54
Source documentation
Split along any vector of nonzero norm; this bounds a norm sphere by exactly two choices over every point of the orthogonal complement.
```
theorem norm_sphere_count (B : LinearMap.BilinForm K E) (hs : B.IsSymm)
    (x : E) (hx : B x x ≠ 0) (a : K) :
    Nat.card {v : E // B v v = a} ≤
      2 * Nat.card (B.orthogonal (K ∙ x)) := by
…
```
theorem OAI.SidorenkoCounterexample.norm_sphere_count_pow line 96
def OAI.SidorenkoCounterexample.BilinAut line 113
Source documentation
Linear automorphisms preserving a specified bilinear form.
```
def BilinAut (B : LinearMap.BilinForm K E) :=
…
```
instance OAI.SidorenkoCounterexample.(instance at line 116) line 116
def OAI.SidorenkoCounterexample.restrictBilinAut line 122
theorem OAI.SidorenkoCounterexample.restrictBilinAut_apply line 146
theorem OAI.SidorenkoCounterexample.restrictBilinAut_injective line 153
Source documentation
An isometry fixing a nonzero-norm vector is determined by its action on the orthogonal complement.
```
theorem restrictBilinAut_injective (B : LinearMap.BilinForm K E)
    (x : E) (hx : B x x ≠ 0) :
    Function.Injective (fun e : {e : BilinAut B // e.val x = x} =>
      restrictBilinAut B x e.val e.property) := by
…
```
Mentions: OAI.SidorenkoCounterexample.BilinAut, OAI.SidorenkoCounterexample.restrictBilinAut
def OAI.SidorenkoCounterexample.relativeBilinAut line 172
theorem OAI.SidorenkoCounterexample.relativeBilinAut_injective line 181
theorem OAI.SidorenkoCounterexample.bilinAut_eval_fiber_bound line 194
Source documentation
The fibers of evaluation at x inject into the stabilizer of x by translation by any chosen member of the fiber.
```
theorem bilinAut_eval_fiber_bound (B : LinearMap.BilinForm K E) (x y : E)
    (hx : B x x ≠ 0) :
    Nat.card {e : BilinAut B // e.val x = y} ≤
      Nat.card (BilinAut (B.restrict (B.orthogonal (K ∙ x)))) := by
…
```
Mentions: OAI.SidorenkoCounterexample.BilinAut
theorem OAI.SidorenkoCounterexample.bilinAut_step line 219
Source documentation
A nonzero-norm vector splits the cardinality estimate into its norm sphere and the isometries of the smaller orthogonal complement.
```
theorem bilinAut_step (B : LinearMap.BilinForm K E) (x : E) (hx : B x x ≠ 0) :
    Nat.card (BilinAut B) ≤ Nat.card {y : E // B y y = B x x} *
      Nat.card (BilinAut (B.restrict (B.orthogonal (K ∙ x)))) := by
…
```
Mentions: OAI.SidorenkoCounterexample.BilinAut
theorem OAI.SidorenkoCounterexample.bilinAut_card_bound line 238

def OAI.SidorenkoCounterexample.linearAutTuple line 298

Source documentation

Evaluate a linear automorphism on a fixed basis.

noncomputable def linearAutTuple : (E ≃ₗ[K] E) →
    {v : Fin (finrank K E) → E // LinearIndependent K v} := fun e =>
…

theorem OAI.SidorenkoCounterexample.linearAutTuple_bijective line 303
theorem OAI.SidorenkoCounterexample.linearAut_card line 323
Source documentation
General linear group order, obtained directly by counting ordered bases.
```
theorem linearAut_card : Nat.card (E ≃ₗ[K] E) =
    ∏ i : Fin (finrank K E), (Fintype.card K ^ finrank K E - Fintype.card K ^ i.val) := by
…
```
abbrev OAI.SidorenkoCounterexample.FormOrbit line 329
Source documentation
The congruence orbit of the literal form, not merely its rank stratum.
```
abbrev FormOrbit (B : LinearMap.BilinForm K E) :=
…
```
instance OAI.SidorenkoCounterexample.linearAut_finite line 332
instance OAI.SidorenkoCounterexample.formOrbit_finite line 336
def OAI.SidorenkoCounterexample.formOrbitMap line 343
theorem OAI.SidorenkoCounterexample.formOrbit_fiber_bound line 349
Source documentation
Every orbit-map fiber embeds into the isometry group; this is the inequality direction of orbit--stabilizer, without assuming a form classification.
```
theorem formOrbit_fiber_bound (B : LinearMap.BilinForm K E) (C : FormOrbit B) :
    Nat.card {e : E ≃ₗ[K] E // formOrbitMap B e = C} ≤ Nat.card (BilinAut B) := by
…
```
Mentions: OAI.SidorenkoCounterexample.FormOrbit, OAI.SidorenkoCounterexample.formOrbitMap, OAI.SidorenkoCounterexample.BilinAut
theorem OAI.SidorenkoCounterexample.formOrbit_card_mul_bound line 370
theorem OAI.SidorenkoCounterexample.linearAut_card_lower line 376
theorem OAI.SidorenkoCounterexample.formOrbit_card_lower line 402
Source documentation
Every nonsingular symmetric form class occupies a fixed positive proportion of the full symmetric-form space, uniformly in the finite field. The deliberately coarse constant 4⁻ᵈ is enough for the manuscript's tail bound.
```
theorem formOrbit_card_lower (B : LinearMap.BilinForm K E) (hs : B.IsSymm)
    (hB : B.Nondegenerate) :
    Fintype.card K ^ (finrank K E+1).choose 2 ≤
      4 ^ finrank K E * Nat.card (FormOrbit B) := by
…
```
Mentions: OAI.SidorenkoCounterexample.FormOrbit
theorem OAI.SidorenkoCounterexample.fullGraph_selforthogonal line 440
Source documentation
Graph coordinates for a transverse Lagrangian, with the full symmetric form retained rather than only its dimension or square class.
```
theorem fullGraph_selforthogonal (B : LinearMap.BilinForm K V) (hs : B.IsSymm) :
    canonicalSymplectic.orthogonal B.graph = B.graph := by
…
```
theorem OAI.SidorenkoCounterexample.fullGraph_injective line 457
def OAI.SidorenkoCounterexample.formCoordinateEquiv line 467
Source documentation
The coordinate action corresponding to a change of basis of a form.
```
def formCoordinateEquiv (g : V ≃ₗ[K] V) :
    (V × Module.Dual K V) ≃ₗ[K] (V × Module.Dual K V) :=
…
```
theorem OAI.SidorenkoCounterexample.formCoordinateEquiv_isometry line 471
theorem OAI.SidorenkoCounterexample.fullGraph_congruence line 476

theorem OAI.SidorenkoCounterexample.exists_transverse_triple_form line 498

Source documentation

Three pairwise transverse Lagrangians admit literal symmetric-form coordinates; transversality to both axes is exactly nonsingularity.

theorem exists_transverse_triple_form (ha : ω.IsAlt) (hω : ω.Nondegenerate)
    (L M N : Submodule K E) (hL : ω.orthogonal L = L)
    (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
    (hLM : L ⊓ M = ⊥) (hLN : L ⊓ N = ⊥) (hMN : M ⊓ N = ⊥) :
    ∃ (e : (L × Module.Dual K L) ≃ₗ[K] E) (B : LinearMap.BilinForm K L),
      B.IsSymm ∧ B.Nondegenerate ∧
      (∀ x, e x ∈ L ↔ x.2 = 0) ∧ (∀ x, e x ∈ M ↔ x.1 = 0) ∧
      (∀ x, e x ∈ N ↔ x.2 = B x.1) ∧
      (∀ x y, ω (e x) (e y) = canonicalSymplectic x y) := by
…

Mentions: OAI.SidorenkoCounterexample.canonicalSymplectic

abbrev OAI.SidorenkoCounterexample.FixedPairOrbit line 584
Source documentation
Third members reachable while fixing both members of the ordered pair.
```
abbrev FixedPairOrbit := {N' : Submodule K E //
…
```
theorem OAI.SidorenkoCounterexample.fixedPairOrbit_selforthogonal line 588

theorem OAI.SidorenkoCounterexample.fixedPairOrbit_form_injection line 597

Source documentation

Congruence classes inject into the actual third-member fiber of the ordered symplectic orbit. No classification of forms is used.

theorem fixedPairOrbit_form_injection (ha : ω.IsAlt) (hω : ω.Nondegenerate)
    (hL : ω.orthogonal L = L) (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
    (hLM : L ⊓ M = ⊥) (hLN : L ⊓ N = ⊥) (hMN : M ⊓ N = ⊥) :
    ∃ B : LinearMap.BilinForm K L, B.IsSymm ∧ B.Nondegenerate ∧
      ∃ f : FormOrbit B → FixedPairOrbit ω L M N, Function.Injective f := by
…

Mentions: OAI.SidorenkoCounterexample.FormOrbit, OAI.SidorenkoCounterexample.FixedPairOrbit

theorem OAI.SidorenkoCounterexample.fixedPairOrbit_card_lower line 649

Source documentation

The essential residual orbit lower bound, with a concrete uniform fixed-dimension constant, for each individual target ordered triple.

theorem fixedPairOrbit_card_lower (ha : ω.IsAlt) (hω : ω.Nondegenerate)
    (hL : ω.orthogonal L = L) (hM : ω.orthogonal M = M) (hN : ω.orthogonal N = N)
    (hLM : L ⊓ M = ⊥) (hLN : L ⊓ N = ⊥) (hMN : M ⊓ N = ⊥) :
    Fintype.card K ^ (finrank K L+1).choose 2 ≤
      4 ^ finrank K L * Nat.card (FixedPairOrbit ω L M N) := by
…

Mentions: OAI.SidorenkoCounterexample.FixedPairOrbit

theorem OAI.SidorenkoCounterexample.lagrangian_card_by_dimension line 669
Source documentation
Reindexing the exact graph-chart count by projection dimension.
```
theorem lagrangian_card_by_dimension :
    Nat.card (Lagrangian (K := K) (V := V)) =
…
```
Mentions: OAI.SidorenkoCounterexample.Lagrangian
def OAI.SidorenkoCounterexample.lagrangianConstant line 689
Source documentation
A field-independent fixed-dimension upper normalization constant.
```
noncomputable def lagrangianConstant (n : ℕ) : ℝ := (n+1) * 2^n
```
theorem OAI.SidorenkoCounterexample.lagrangianConstant_pos line 691
theorem OAI.SidorenkoCounterexample.lagrangian_card_upper line 695
theorem OAI.SidorenkoCounterexample.lagrangian_card_lower line 725
abbrev OAI.SidorenkoCounterexample.SymplecticLagrangian line 744
abbrev OAI.SidorenkoCounterexample.OrderedTransversePair line 745
abbrev OAI.SidorenkoCounterexample.OrderedTripleOrbit line 747
theorem OAI.SidorenkoCounterexample.orderedTripleOrbit_pair_injection line 754
theorem OAI.SidorenkoCounterexample.transverse_to_card line 804
theorem OAI.SidorenkoCounterexample.orderedTransversePair_card line 821
theorem OAI.SidorenkoCounterexample.orderedTransverseTriple_card_lower line 837