FormGluing.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SidorenkoCounterexample.preimageFiberEquiv line 12
theorem OAI.SidorenkoCounterexample.surjective_linear_preimage_card line 22
theorem OAI.SidorenkoCounterexample.surjective_linear_card line 35
theorem OAI.SidorenkoCounterexample.surjective_linear_probability line 40
def OAI.SidorenkoCounterexample.weightedCombination line 51
theorem OAI.SidorenkoCounterexample.weightedCombination_surjective line 55
theorem OAI.SidorenkoCounterexample.finite_union_card_bound line 70
theorem OAI.SidorenkoCounterexample.finite_union_probability_bound line 79
def OAI.SidorenkoCounterexample.symmetricFormSubmodule line 96
instance OAI.SidorenkoCounterexample.(instance at line 102) line 102
instance OAI.SidorenkoCounterexample.(instance at line 105) line 105
theorem OAI.SidorenkoCounterexample.symmetric_combination_nullity_bound line 111

theorem OAI.SidorenkoCounterexample.symmetric_bad_span_bound line 124

Source documentation

The simultaneous bad-combination event, before invertibility conditioning. The union is over every nonzero frequency, not only a fixed one; its cardinal cost is explicitly q^s.

 theorem symmetric_bad_span_bound (u : ℕ) (hu : u ≤ finrank K V) :
    (Nat.card {Q : ι → SymForm K V // ∃ t : ι → K, t ≠ 0 ∧
      u ≤ finrank K (weightedCombination t Q).val.ker} : ℝ) /
      Nat.card (ι → SymForm K V) ≤
      (Fintype.card K : ℝ)^(Fintype.card ι) *
        (2^u / (Fintype.card K : ℝ)^((u+1).choose 2)) := by
…

Mentions: OAI.SidorenkoCounterexample.SymForm, OAI.SidorenkoCounterexample.weightedCombination

theorem OAI.SidorenkoCounterexample.symmetric_low_rank_span_bound line 152
theorem OAI.SidorenkoCounterexample.symmetric_form_descend line 191
Source documentation
Symmetric forms descend through a linear map precisely when its kernel is in the radical; the result is extended to the ambient codomain.
```
 theorem symmetric_form_descend (f : E →ₗ[K] V) (B : LinearMap.BilinForm K E)
    (hB : B.IsSymm) (hk : f.ker ≤ B.ker) :
    ∃ C : LinearMap.BilinForm K V, C.IsSymm ∧ C.compl₁₂ f f = B := by
…
```
theorem OAI.SidorenkoCounterexample.symmetric_form_extend line 221

def OAI.SidorenkoCounterexample.glueCross line 230

Source documentation

The cross block implementing gluing of forms on two subspaces. Its restrictions to the common subspace agree with the prescribed forms.

def glueCross (U W : Submodule K V) (B : LinearMap.BilinForm K U)
    (C : LinearMap.BilinForm K W)
    (p : U →ₗ[K] ↥(U ⊓ W)) (q : W →ₗ[K] ↥(U ⊓ W)) :
    U →ₗ[K] W →ₗ[K] K :=
…

theorem OAI.SidorenkoCounterexample.glueCross_left line 241
theorem OAI.SidorenkoCounterexample.glueCross_right line 254
theorem OAI.SidorenkoCounterexample.symmetric_form_glue line 275

theorem OAI.SidorenkoCounterexample.symmetric_form_glue_pointwise line 346

Source documentation

Pointwise form of simultaneous extension, avoiding any implicit identification of the two copies of the common subspace.

theorem symmetric_form_glue_pointwise (hB : B.IsSymm) (hC : C.IsSymm)
    (hc : ∀ (x y : V) (hxU : x ∈ U) (hxW : x ∈ W) (hyU : y ∈ U) (hyW : y ∈ W),
      B ⟨x,hxU⟩ ⟨y,hyU⟩ = C ⟨x,hxW⟩ ⟨y,hyW⟩) :
    ∃ F : LinearMap.BilinForm K V, F.IsSymm ∧
      F.compl₁₂ U.subtype U.subtype = B ∧ F.compl₁₂ W.subtype W.subtype = C := by
…

theorem OAI.SidorenkoCounterexample.cyclic_difference_exists line 362
def OAI.SidorenkoCounterexample.symFormPull line 438
theorem OAI.SidorenkoCounterexample.symFormPull_surjective line 443
abbrev OAI.SidorenkoCounterexample.DifferenceTargets line 451
abbrev OAI.SidorenkoCounterexample.CommonSpace line 453
def OAI.SidorenkoCounterexample.commonInclusion₀ line 455
def OAI.SidorenkoCounterexample.commonInclusion₁ line 457
def OAI.SidorenkoCounterexample.commonInclusion₂ line 459
def OAI.SidorenkoCounterexample.cyclicDifferenceMap line 462
def OAI.SidorenkoCounterexample.differenceConstraint line 469
theorem OAI.SidorenkoCounterexample.differenceConstraint_surjective line 477
theorem OAI.SidorenkoCounterexample.cyclicDifference_range line 491
Source documentation
The exact image, with all common-space constraints retained.
```
theorem cyclicDifference_range :
    (cyclicDifferenceMap A₀ A₁ A₂).range = (differenceConstraint A₀ A₁ A₂).ker := by
…
```
Mentions: OAI.SidorenkoCounterexample.cyclicDifferenceMap, OAI.SidorenkoCounterexample.differenceConstraint
theorem OAI.SidorenkoCounterexample.linear_constraint_probability_bound line 537
Source documentation
Conditioning a uniform vector on a surjective linear constraint costs at most the cardinality of the constraint space. This is a counting inequality, not an independence assumption about the constrained entries.
```
theorem linear_constraint_probability_bound (f : U →ₗ[K] W) (c : W →ₗ[K] X)
    (hc : Function.Surjective c) (hfc : f.range = c.ker) (P : W → Prop) :
    (Nat.card {u : U // P (f u)} : ℝ) / Nat.card U ≤
      (Nat.card X : ℝ) * (Nat.card {w : W // P w} : ℝ) / Nat.card W := by
…
```
def OAI.SidorenkoCounterexample.triplePredicateEquiv line 567
theorem OAI.SidorenkoCounterexample.triple_predicate_probability line 576
abbrev OAI.SidorenkoCounterexample.OriginalForms line 594
def OAI.SidorenkoCounterexample.ambientRestrictions line 596
def OAI.SidorenkoCounterexample.originalCyclicDifference line 602
theorem OAI.SidorenkoCounterexample.ambientRestrictions_surjective line 616
theorem OAI.SidorenkoCounterexample.originalDifference_comp_restriction line 625
theorem OAI.SidorenkoCounterexample.originalCyclicDifference_range line 644
Source documentation
The image statement for exactly the independent form spaces appearing in the planted lift, NOT an assumption of independent difference matrices.
```
theorem originalCyclicDifference_range :
    (originalCyclicDifference A₀ A₁ A₂).range = (differenceConstraint A₀ A₁ A₂).ker := by
…
```
Mentions: OAI.SidorenkoCounterexample.originalCyclicDifference, OAI.SidorenkoCounterexample.differenceConstraint
theorem OAI.SidorenkoCounterexample.planted_nullity_probability_bound line 654
theorem OAI.SidorenkoCounterexample.lift_pair_profile_probability_bound line 691