production module

`AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Geometry/EuclideanSpaceCoordinates.lean.

Imports

Mathlib.Analysis.InnerProductSpace.PiL2 externalMathlib.Tactic.Ring external

Imported by

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAutoSamplingTheory.TechnicalLemmas.GeometryAutoSamplingTheory.TechnicalLemmas.RegistryAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoFormulaAlgebraAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_toLp_toLp_eq_sum_mul Compiled Not mapped

- Inner product of two real coordinate functions after the `EuclideanSpace` `WithLp.toLp 2` embedding.

theorem euclideanSpace_inner_toLp_toLp_eq_sum_mul
    {ι : Type*} [Fintype ι] (u v : ι → ℝ) :
    inner ℝ (WithLp.toLp 2 u : EuclideanSpace ℝ ι)
        (WithLp.toLp 2 v : EuclideanSpace ℝ ι) =
      ∑ i, u i * v i := by
  rw [PiLp.inner_apply]
  refine Finset.sum_congr rfl ?_
  intro i _
  change v i * u i = u i * v i
  ring

/-- Inner product of two real `EuclideanSpace` vectors in coordinates. -/

AutoSamplingTheory/TechnicalLemmas/Geometry/EuclideanSpaceCoordinates.lean:21published source at 77184245109aOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul Compiled Not mapped

- Inner product of two real `EuclideanSpace` vectors in coordinates.

theorem euclideanSpace_inner_eq_sum_mul
    {ι : Type*} [Fintype ι] (u v : EuclideanSpace ℝ ι) :
    inner ℝ u v = ∑ i, u i * v i := by
  rw [PiLp.inner_apply]
  refine Finset.sum_congr rfl ?_
  intro i _
  change v i * u i = u i * v i
  ring

end EuclideanSpaceCoordinates
end Geometry
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Geometry/EuclideanSpaceCoordinates.lean:33published source at 77184245109aOpen detailed card