Mathematics · proofs · software

Special Functions · Lean source

CoupledCharacteristicAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

Local imports (1)

CoupledCharacteristicAudit.lean25 lines

Original source pathlean/CoupledCharacteristicAudit.lean

Skip source text

1 import CoupledCharacteristic
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_zero
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.rpow_contraction_bounds
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_continuous
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_strictMono
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicBalance_tendsto
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_exponent_exists_unique
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicExponent_spec
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicVector_positive
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicLeftVector_positive
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_right_eigenvector
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_left_eigenvector
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristicNormalizer_positive
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_positive
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.normalizedCharacteristicVector_max
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.normalized_characteristic_eigenvector
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_second_eigenvalue_bound
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectralRadius
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_mem_spectrum_iff
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum_real
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectrum_norm_attained
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectralRadius_iff
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_spectral_exponent_exists_unique

Back to source controls

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: c6871063f94b1e70dc1656737863d91eef847dc6f5f39e0a048ccdadaf496cf0

Original source on GitHub

Back to Special Functions