SigmaNormalization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.adjointEquiv line 18
Source comment
The genuine adjoint equivalence of a transverse linear normalization.
```
def adjointEquiv (A : E ≃L[ℝ] E) : E ≃L[ℝ] E :=
…
```
lemma OAI.AffineBernstein.homogeneousSupport_linear_image line 30
lemma OAI.AffineBernstein.adjointEquiv_inv_apply line 39
lemma OAI.AffineBernstein.prod_image_fiber line 48

lemma OAI.AffineBernstein.support_normalized_pullback line 63

Source comment

The support of the actual normalized fiber, pulled back by inverse-adjoint normal variables, is the original support. No fiber hypothesis is used.

lemma support_normalized_pullback {S : Type*} [NormedAddCommGroup S] [NormedSpace ℝ S]
    (B : S ≃L[ℝ] S) (A : E ≃L[ℝ] E) (C : Set (S × E)) :
    (fun q : S × E => homogeneousSupport {y | (B q.1,y) ∈ (B.prodCongr A) '' C}
      (adjointEquiv A.symm q.2)) =
    (fun q : S × E => homogeneousSupport {y | (q.1,y) ∈ C} q.2) := by
…

Mentions: OAI.AffineBernstein.homogeneousSupport, OAI.AffineBernstein.adjointEquiv