theorem AddChar.map_finsetSum.{u_1, u_2, u_3}
  {ι : Type u_1} {A : Type u_2}
  {M : Type u_3} [AddCommMonoid A]
  [CommMonoid M] (ψ : AddChar A M)
  (s : Finset ι) (f : ι → A) :
  ψ (∑ i ∈ s, f i) = ∏ i ∈ s, ψ (f i)

theorem ZMod.sum_stdAddChar_mul {N : ℕ} [NeZero N]
  (t : ZMod N) :
  ∑ c, ZMod.stdAddChar (c * t) =
    if t = 0 then ↑N else 0

theorem ZMod.norm_stdAddChar {N : ℕ} [NeZero N]
  (z : ZMod N) : ‖ZMod.stdAddChar z‖ = 1

theorem ZMod.conj_stdAddChar {N : ℕ} [NeZero N]
  (z : ZMod N) :
  (starRingEnd ℂ) (ZMod.stdAddChar z) =
    ZMod.stdAddChar (-z)

theorem ZMod.sum_dft_mul_dft_mul_stdAddChar
  {N : ℕ} [NeZero N] (u v : ZMod N → ℂ)
  (t : ZMod N) :
  ∑ ω,
      ZMod.dft u ω * ZMod.dft v ω *
        ZMod.stdAddChar (ω * t) =
    ↑N * ∑ b, u b * v (t - b)

theorem ZMod.piDFT_apply_zero.{u_1, u_2} {N : ℕ}
  [NeZero N] {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {E : Type u_2}
  [AddCommGroup E] [Module ℂ E]
  (f : (ι → ZMod N) → E) :
  ZMod.piDFT f 0 = ∑ x, f x

theorem ZMod.sum_stdAddChar_dotProduct.{u_1}
  {N : ℕ} [NeZero N] {ι : Type u_1}
  [Fintype ι] [DecidableEq ι]
  (t : ι → ZMod N) :
  ∑ ξ, ZMod.stdAddChar (ξ ⬝ᵥ t) =
    if t = 0 then ↑N ^ Fintype.card ι
    else 0

theorem ZMod.sum_stdAddChar_smul_piDFT.{u_1, u_2}
  {N : ℕ} [NeZero N] {ι : Type u_1}
  [Fintype ι] [DecidableEq ι]
  {E : Type u_2} [AddCommGroup E]
  [Module ℂ E] (f : (ι → ZMod N) → E)
  (x : ι → ZMod N) :
  ∑ ξ,
      ZMod.stdAddChar (ξ ⬝ᵥ x) •
        ZMod.piDFT f ξ =
    ↑N ^ Fintype.card ι • f x

theorem ZMod.piDFT_inversion.{u_1, u_2} {N : ℕ}
  [NeZero N] {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {E : Type u_2}
  [AddCommGroup E] [Module ℂ E]
  (f : (ι → ZMod N) → E)
  (x : ι → ZMod N) :
  f x =
    (↑N ^ Fintype.card ι)⁻¹ •
      ∑ ξ,
        ZMod.stdAddChar (ξ ⬝ᵥ x) •
          ZMod.piDFT f ξ

theorem MeasureTheory.measurePreserving_planeOrthogonalSplit.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (L :
    EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) :
  MeasureTheory.MeasurePreserving
    (⇑(MeasureTheory.planeOrthogonalSplit
        L))
    MeasureTheory.volume
    MeasureTheory.volume

theorem MeasureTheory.inner_planeOrthogonalSplit.{u_1}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E)
  (b ω : EuclideanSpace ℝ (Fin k))
  (y : ↥L.rangeᗮ) :
  inner ℝ (L b + ↑y) (L ω) = inner ℝ b ω

theorem MeasureTheory.integrable_comp_planeOrthogonalSplit.{u_1,
    u_2}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (L :
    EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) :
  MeasureTheory.Integrable
    (fun by_ ↦ f (L by_.1 + ↑by_.2))
    MeasureTheory.volume

theorem MeasureTheory.ae_integrable_dPlaneTransform_section.{u_1,
    u_2}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (L :
    EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) :
  ∀ᵐ (b : EuclideanSpace ℝ (Fin k)),
    MeasureTheory.Integrable
      (fun y ↦ f (L b + ↑y))
      MeasureTheory.volume

theorem MeasureTheory.integrable_dPlaneTransform.{u_1,
    u_2}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (L :
    EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) :
  MeasureTheory.Integrable
    (MeasureTheory.dPlaneTransform f L)
    MeasureTheory.volume

theorem MeasureTheory.integral_dPlaneTransform.{u_1,
    u_2}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (L :
    EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E) :
  ∫ (b : EuclideanSpace ℝ (Fin k)),
      MeasureTheory.dPlaneTransform f L
        b =
    ∫ (x : E), f x

theorem MeasureTheory.fourier_slice_dPlaneTransform.{u_1,
    u_3}
  {k : ℕ} {E : Type u_1}
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F' : Type u_3} [NormedAddCommGroup F']
  [NormedSpace ℂ F'] {f : E → F'}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (L : EuclideanSpace ℝ (Fin k) →ₗᵢ[ℝ] E)
  (ω : EuclideanSpace ℝ (Fin k)) :
  FourierTransform.fourier f (L ω) =
    FourierTransform.fourier
      (MeasureTheory.dPlaneTransform f L)
      ω

theorem MeasureTheory.norm_frameVectorCodimOne.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L :
    EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) :
  ‖MeasureTheory.frameVectorCodimOne L‖ =
    1

theorem MeasureTheory.eq_smul_single_fin_one
  (b : EuclideanSpace ℝ (Fin 1)) :
  b = b.ofLp 0 • EuclideanSpace.single 0 1

theorem MeasureTheory.apply_eq_smul_frameVectorCodimOne.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E)
  (b : EuclideanSpace ℝ (Fin 1)) :
  L b =
    b.ofLp 0 •
      MeasureTheory.frameVectorCodimOne L

theorem MeasureTheory.range_eq_span_frameVectorCodimOne.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L :
    EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E) :
  L.range =
    ℝ ∙
      MeasureTheory.frameVectorCodimOne L

theorem MeasureTheory.dPlaneTransform_codimOne.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (f : E → F)
  (L : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E)
  (b : EuclideanSpace ℝ (Fin 1)) :
  MeasureTheory.dPlaneTransform f L b =
    MeasureTheory.radonTransform f
      (MeasureTheory.frameVectorCodimOne
        L)
      (b.ofLp 0)

theorem MeasureTheory.norm_eq_abs_apply_fin_one
  (b : EuclideanSpace ℝ (Fin 1)) :
  ‖b‖ = |b.ofLp 0|

theorem MeasureTheory.frameOfUnitVector_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (u : ↑(Metric.sphere 0 1))
  (b : EuclideanSpace ℝ (Fin 1)) :
  (MeasureTheory.frameOfUnitVector u) b =
    b.ofLp 0 • ↑u

theorem MeasureTheory.frameVectorCodimOne_frameOfUnitVector.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (u : ↑(Metric.sphere 0 1)) :
  MeasureTheory.frameVectorCodimOne
      (MeasureTheory.frameOfUnitVector
        u) =
    ↑u

theorem MeasureTheory.frameOfUnitVector_frameVectorCodimOne.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (L : EuclideanSpace ℝ (Fin 1) →ₗᵢ[ℝ] E)
  (hL :
    ‖MeasureTheory.frameVectorCodimOne
          L‖ =
      1) :
  MeasureTheory.frameOfUnitVector
      ⟨MeasureTheory.frameVectorCodimOne
          L,
        ⋯⟩ =
    L

theorem MeasureTheory.coe_unitVectorFinOne :
  ↑MeasureTheory.unitVectorFinOne =
    EuclideanSpace.single 0 1

theorem MeasureTheory.integral_euclideanSpace_fin_one.{u_3}
  {G : Type u_3} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (g : ℝ → G) :
  ∫ (b : EuclideanSpace ℝ (Fin 1)),
      g (b.ofLp 0) =
    ∫ (t : ℝ), g t

theorem MeasureTheory.diagScale_apply {k : ℕ}
  (w : Fin k → ℝ)
  (d : EuclideanSpace ℝ (Fin k))
  (i : Fin k) :
  ((MeasureTheory.diagScale w) d).ofLp i =
    w i * d.ofLp i

theorem MeasureTheory.det_diagScale {k : ℕ}
  (w : Fin k → ℝ) :
  LinearMap.det
      (MeasureTheory.diagScale w) =
    ∏ i, w i

theorem MeasureTheory.coe_diagScaleMeasurableEquiv
  {k : ℕ} {w : Fin k → ℝ}
  (hw : ∀ (i : Fin k), w i ≠ 0)
  (d : EuclideanSpace ℝ (Fin k)) :
  (MeasureTheory.diagScaleMeasurableEquiv
        hw)
      d =
    (MeasureTheory.diagScale w) d

theorem MeasureTheory.integral_comp_diagScale.{u_1}
  {k : ℕ} {G : Type u_1}
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  {w : Fin k → ℝ}
  (hw : ∀ (i : Fin k), w i ≠ 0)
  (G' : EuclideanSpace ℝ (Fin k) → G) :
  ∫ (d : EuclideanSpace ℝ (Fin k)),
      G' ((MeasureTheory.diagScale w) d) =
    (∏ i, |w i|)⁻¹ •
      ∫ (y : EuclideanSpace ℝ (Fin k)),
        G' y