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

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_toLp_toLp_eq_sum_mul Partial 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 ed709a7f320dOpen detailed card

theorem AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates.euclideanSpace_inner_eq_sum_mul Partial 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 ed709a7f320dOpen detailed card

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Geometry/EuclideanSpaceCoordinates.lean — full module with imports and context

Download module (.lean)

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Tactic.Ring

/-!
# Euclidean-space coordinate bridges

Small reusable coordinate identities for finite-dimensional Euclidean spaces.
These leaves are purely linear-algebraic notation bridges; they do not define
gradients, divergence, Hessians, Laplacians, or analytic regularity.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace Geometry
namespace EuclideanSpaceCoordinates

open scoped BigOperators RealInnerProductSpace

/-- 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. -/
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