Mathematics · proofs · software

Special Functions · Lean source

CoupledTypeProportionsAudit.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)

CoupledTypeProportionsAudit.lean28 lines

Original source pathlean/CoupledTypeProportionsAudit.lean

Skip source text

1 import CoupledTypeProportions
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.affine_scale_tendsto
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.affine_power_ratio_tendsto
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lower_comparison_of_tendsto
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upper_comparison_of_tendsto
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_envelopes
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scaled_log_factorization
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.scaled_type_envelopes
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.log_power_correction_tendsto
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lower_type_row
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.upper_type_row
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_lower_type_superinvariant
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_upper_type_subinvariant
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.positive_dot_rigidity
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.left_eigenvector_preserves_dot
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_fixed_vectors
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_fixed_proportion
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_proportions
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_positive_type_proportions
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.characteristic_fixed_ratios
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_ratios
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.ordinary_type_limit_iff
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.type_equality_iff_scalar_equality
25 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_limit_equivalence
26 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_limit_vector
27 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_proportions
28 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_limit_equivalence

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: 4532e08e1efa4619f56e134e53a29e6a3b94a6bf7b2d284531f912f0640ebe3f

Original source on GitHub

Back to Special Functions