Mathematics · proofs · software

Special Functions · Lean source

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

CoupledPositiveRealAudit.lean24 lines

Original source pathlean/CoupledPositiveRealAudit.lean

Skip source text

1 import CoupledPositiveReal
2 
3 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_series_hasSum
4 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_identification
5 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_zero
6 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_nonneg
7 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_lower_linear
8 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_hasDerivAt
9 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_differentiable
10 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_deriv_ge_one
11 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_strictMono
12 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_positive
13 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.odd_series_norm_le_real_sum
14 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.complex_norm_le_real_axis
15 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_norm
16 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.sphere_norm_isGreatest
17 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.maximum_modulus_real_axis
18 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.unit_shift_lower_from_deriv
19 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_unit_lower
20 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.real_axis_log_unit_lower
21 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.minScale_bounds
22 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.minScale_positive
23 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lowerThreshold_gt_one
24 #print axioms Komorebi.SpecialFunctions.Coupled.Scales.lower_child_radii

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: 49a920db319b72249aa31058c6f492238dbe239de18644defccc4dad6f25bdbe

Original source on GitHub

Back to Special Functions