HyperplaneJacobian.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.ProjectionCounterexample.perpendicularTo line 17
def OAI.ProjectionCounterexample.hyperplaneProjection line 20
Source documentation
Restrict the actual orthogonal projection to the source tangent hyperplane.
```
def hyperplaneProjection (n u : V) : perpendicularTo n →ₗ[ℝ] V :=
…
```
Mentions: OAI.ProjectionCounterexample.perpendicularTo
theorem OAI.ProjectionCounterexample.perpendicularTo_finrank line 23
theorem OAI.ProjectionCounterexample.perpendicularTo_projection_apply line 34
theorem OAI.ProjectionCounterexample.inner_perpendicularTo_projection line 40
theorem OAI.ProjectionCounterexample.hyperplaneProjection_normDet line 50
Source documentation
The projected facet's area factor is the absolute inner product of unit normals.
```
theorem hyperplaneProjection_normDet {n u : V} (hn : ‖n‖ = 1) (hu : ‖u‖ = 1) :
    (hyperplaneProjection n u).normDet = |⟪n, u⟫| := by
…
```
Mentions: OAI.ProjectionCounterexample.hyperplaneProjection

theorem OAI.ProjectionCounterexample.normDet_project_comp line 104

Source documentation

The same area factor for any linear chart into the source tangent hyperplane. The chart may be singular; the norm determinant identity handles that case as well.

theorem normDet_project_comp {U : Type*} [NormedAddCommGroup U] [InnerProductSpace ℝ U]
    [FiniteDimensional ℝ U] (L : U →ₗ[ℝ] V) {n u : V}
    (hn : ‖n‖ = 1) (hu : ‖u‖ = 1)
    (hmem : ∀ x, ⟪n, L x⟫ = 0)
    (hrank : Module.finrank ℝ U = Module.finrank ℝ V - 1) :
    ((perpendicularTo u).starProjection.toLinearMap.comp L).normDet =
      |⟪n, u⟫| * L.normDet := by
…

Mentions: OAI.ProjectionCounterexample.perpendicularTo

theorem OAI.ProjectionCounterexample.hyperplaneProjection_measure_image line 127
theorem OAI.ProjectionCounterexample.hyperplaneProjection_measure_translated line 135