Komorebi Space · Lean source
DiagonalDefinitions.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
KomorebiSpace/DiagonalDefinitions.lean22 lines
Original source path
lean/KomorebiSpace/DiagonalDefinitions.leanSkip declarations and read code
1 import Mathlib.Topology.Algebra.InfiniteSum.Real
2 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3
4 set_option autoImplicit false
5 noncomputable section
6 namespace KomorebiSpace.DiagonalRegularization
7
8 /-- Natural index `j` denotes the printed positive coordinate `j+1`. -/
9 def index (j : ℕ) : ℝ := (j : ℝ) + 1
10
11 def aCoord (m j : ℕ) : ℝ := (m : ℝ)^2 / ((m : ℝ)^2 + (index j)^2)
12 def vCoord (m j : ℕ) : ℝ := index j / ((m : ℝ)^2 + (index j)^2)
13 def cCoord (m j : ℕ) : ℝ := (m : ℝ)^2 / (index j * ((m : ℝ)^2 + (index j)^2))
14 def wCoord (j : ℕ) : ℝ := (index j)⁻¹
15 def bCoord (j : ℕ) : ℝ := ((index j)^2)⁻¹
16
17 def A (m : ℕ) : ℝ := ∑' j, (aCoord m j)^2
18 def B (m : ℕ) : ℝ := ∑' j, (vCoord m j)^2
19 def partialA (m K : ℕ) : ℝ := ∑ j ∈ Finset.range K, (aCoord m j)^2
20 def partialB (m K : ℕ) : ℝ := ∑ j ∈ Finset.range K, (vCoord m j)^2
21
22 end KomorebiSpace.DiagonalRegularization
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 751bf02816f74e2fe8a8bc9f45c22f9538d087d1af536af3835e4906f4015f54