RowErasureSliceQuotient.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Every nonempty affine row/column slice is an affine copy of the full space of linear maps from the column quotient into the row kernel. This gives exact uniform-law transport and preserves the affine evaluation offset.

def OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.direction line 21
Source documentation
The linear part of the affine parametrization.
```
def direction (A : K →ₗ[R] L) (Q : Submodule R E)
    (N : (E ⧸ Q) →ₗ[R] A.ker) : E →ₗ[R] K :=
…
```
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.direction_apply line 25
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.exists_direction_of_row_and_column line 31
Source documentation
Quotient descent of a linear map which vanishes on the column span and takes values in the common row kernel.
```
theorem exists_direction_of_row_and_column (A : K →ₗ[R] L)
    (Q : Submodule R E) (B : E →ₗ[R] K)
    (hQ : Q ≤ B.ker) (hA : LinearMap.range B ≤ A.ker) :
    ∃ N : (E ⧸ Q) →ₗ[R] A.ker, direction A Q N = B := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.direction
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.direction_injective line 47
def OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.AffineSlice line 57
Source documentation
The concrete affine slice around any one point satisfying its equations.
```
def AffineSlice (A : K →ₗ[R] L) (Q : Submodule R E) (M₀ : E →ₗ[R] K) :=
…
```
def OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.ofQuotient line 60
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.ofQuotient_val line 72
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.ofQuotient_bijective line 76
def OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.equiv line 100
Source documentation
Uniform free quotient maps parametrize exactly the original affine slice.
```
def equiv (A : K →ₗ[R] L) (Q : Submodule R E) (M₀ : E →ₗ[R] K) :
    ((E ⧸ Q) →ₗ[R] A.ker) ≃ AffineSlice A Q M₀ :=
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.AffineSlice
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.equiv_apply line 104
theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.equiv_affine_target line 109
Source documentation
The base point contributes an affine offset; it is not discarded.
```
theorem equiv_affine_target (A : K →ₗ[R] L) (Q : Submodule R E)
    (M₀ : E →ₗ[R] K) (N : (E ⧸ Q) →ₗ[R] A.ker) (z : E) (u : K) :
    (equiv A Q M₀ N).val z + u =
      (N (Q.mkQ z) : K) + (M₀ z + u) := by
…
```
Mentions: OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.equiv

theorem OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.expect_equiv line 117

Source documentation

Exact uniform-law transport through the affine parametrization.

theorem expect_equiv (A : K →ₗ[R] L) (Q : Submodule R E) (M₀ : E →ₗ[R] K)
    [Fintype ((E ⧸ Q) →ₗ[R] A.ker)] [Fintype (AffineSlice A Q M₀)]
    (f : AffineSlice A Q M₀ → ℝ) :
    Finset.univ.expect (fun N => f (equiv A Q M₀ N)) = Finset.univ.expect f := by
…

Mentions: OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.AffineSlice, OAI.MaxCutGames.Inverse.RowErasureSliceQuotient.equiv