Mathematics · proofs · software

Special Functions · Lean source

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

CoupledGrowthTypesAudit.lean24 lines

Original source pathlean/CoupledGrowthTypesAudit.lean

Skip source text

1 import CoupledGrowthTypes
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.realComponent_positive
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_bounds
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_eventually
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_growth_ratio_bounded
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_type_sandwich
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_type_bounds
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_types_positive
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.loglog_ratio_sandwich
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.tendsto_loglog_of_ratio_bounds
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_radial_exponent_limit
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_radial_order
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_spherical_maximum
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.component_real_norm
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.norm_growth_ratio_eventually_eq
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.norm_type_identification
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_norm_radial_limit
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maximumModulus_eq
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maximum_growth_ratio_eventually_eq
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maximum_type_identification
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_type_bounds
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_radial_limit
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.canonical_maximum_order

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: 92e54ca0a72c76e6ede67b590a1152f7de3eed5c21f226a1fbe56c942d93e1fe

Original source on GitHub

Back to Special Functions