KernelAudit.lean

1 import KomorebiPaperVI
2 
3 #print axioms KomorebiPaperVI.Algebra.block_reconstruction
4 #print axioms KomorebiPaperVI.Algebra.block_multiplication
5 #print axioms KomorebiPaperVI.Algebra.packet_semigroup_convolution
6 #print axioms KomorebiPaperVI.Algebra.difference_idempotent
7 #print axioms KomorebiPaperVI.Algebra.difference_annihilates_coarse
8 #print axioms KomorebiPaperVI.Algebra.tower_telescope
9 #print axioms KomorebiPaperVI.Algebra.intertwining_powers
10 #print axioms KomorebiPaperVI.Algebra.finite_horizon_defect
11 #print axioms KomorebiPaperVI.Algebra.rectangular_resolvent_identity
12 #print axioms KomorebiPaperVI.BanachDefects.duhamel_derivative
13 #print axioms KomorebiPaperVI.BanachDefects.duhamel
14 #print axioms KomorebiPaperVI.BanachDefects.contraction_bound
15 #print axioms KomorebiPaperVI.BayesianFlow.positive_evidence
16 #print axioms KomorebiPaperVI.BayesianFlow.flow_probability
17 #print axioms KomorebiPaperVI.BayesianFlow.likelihood_add
18 #print axioms KomorebiPaperVI.BayesianFlow.flow_add
19 #print axioms KomorebiPaperVI.BayesianFlow.flow_zero
20 #print axioms KomorebiPaperVI.BayesianFlow.likelihood_derivative
21 #print axioms KomorebiPaperVI.BayesianFlow.evidence_derivative
22 #print axioms KomorebiPaperVI.BayesianFlow.flow_derivative
23 #print axioms KomorebiPaperVI.BayesianNecessity.pair_weighted_sum
24 #print axioms KomorebiPaperVI.BayesianNecessity.pair_probability
25 #print axioms KomorebiPaperVI.BayesianNecessity.pair_fiber_weight
26 #print axioms KomorebiPaperVI.BayesianNecessity.pair_coarsen
27 #print axioms KomorebiPaperVI.BayesianNecessity.pair_coarse_posterior
28 #print axioms KomorebiPaperVI.BayesianNecessity.cross_packet_ratio
29 #print axioms KomorebiPaperVI.BayesianNecessity.all_packet_ratio
30 #print axioms KomorebiPaperVI.BayesianNecessity.positive_evidence
31 #print axioms KomorebiPaperVI.BayesianNecessity.refinement_iff
32 #print axioms KomorebiPaperVI.BayesianPartitions.packetMap_surjective
33 #print axioms KomorebiPaperVI.BayesianPartitions.packetLikelihood_apply
34 #print axioms KomorebiPaperVI.BayesianPartitions.packet_eq_iff
35 #print axioms KomorebiPaperVI.BayesianPartitions.packetLikelihood_positive
36 #print axioms KomorebiPaperVI.BayesianPartitions.canonical_coarsening
37 #print axioms KomorebiPaperVI.BayesianPartitions.canonical_unique_factor
38 #print axioms KomorebiPaperVI.BayesianPartitions.all_prior_family_iff_resolves
39 #print axioms KomorebiPaperVI.BayesianPartitions.canonical_coarsest_nontrivial
40 #print axioms KomorebiPaperVI.BayesianPartitions.canonical_nontrivial
41 #print axioms KomorebiPaperVI.BayesianTowers.coarsen_comp
42 #print axioms KomorebiPaperVI.BayesianTowers.singleton_commutes
43 #print axioms KomorebiPaperVI.BayesianTowers.adjacent_criterion
44 #print axioms KomorebiPaperVI.BayesianTowers.compose_commutes
45 #print axioms KomorebiPaperVI.BayesianTowers.coarsen_id
46 #print axioms KomorebiPaperVI.BayesianTowers.tower_commutes
47 #print axioms KomorebiPaperVI.BayesianTowers.tower_criterion
48 #print axioms KomorebiPaperVI.BetaNormalization.beta_value
49 #print axioms KomorebiPaperVI.BetaNormalization.change_derivative
50 #print axioms KomorebiPaperVI.BetaNormalization.change_injective
51 #print axioms KomorebiPaperVI.BetaNormalization.change_image
52 #print axioms KomorebiPaperVI.BetaNormalization.change_integrand
53 #print axioms KomorebiPaperVI.BetaNormalization.rational_integral
54 #print axioms KomorebiPaperVI.BetaNormalization.normalizer_exact
55 #print axioms KomorebiPaperVI.BetaNormalization.sine_factor_positive
56 #print axioms KomorebiPaperVI.BetaNormalization.scalar_fractional_integral
57 #print axioms KomorebiPaperVI.BetaNormalization.beta_real_integral
58 #print axioms KomorebiPaperVI.BetaNormalization.weighted_beta_value
59 #print axioms KomorebiPaperVI.BetaNormalization.gap_change_integrand
60 #print axioms KomorebiPaperVI.BetaNormalization.unit_gap_integral
61 #print axioms KomorebiPaperVI.BetaNormalization.gap_integral
62 #print axioms KomorebiPaperVI.BetaNormalization.normalized_gap_integral
63 #print axioms KomorebiPaperVI.CanonicalJets.calculus_on_component
64 #print axioms KomorebiPaperVI.CanonicalJets.power_kills
65 #print axioms KomorebiPaperVI.CanonicalJets.jet_stable
66 #print axioms KomorebiPaperVI.CanonicalJets.shift_intertwines
67 #print axioms KomorebiPaperVI.CanonicalJets.power_intertwines
68 #print axioms KomorebiPaperVI.CanonicalJets.jet_intertwines
69 #print axioms KomorebiPaperVI.CanonicalJets.canonical_naturality
70 #print axioms KomorebiPaperVI.CanonicalJets.holomorphic_naturality
71 #print axioms KomorebiPaperVI.Coarsening.coarsen_mass
72 #print axioms KomorebiPaperVI.Coarsening.coarsen_nonnegative
73 #print axioms KomorebiPaperVI.Coarsening.coarsen_probability
74 #print axioms KomorebiPaperVI.Coarsening.coarsen_div
75 #print axioms KomorebiPaperVI.Coarsening.coarsen_posterior
76 #print axioms KomorebiPaperVI.Coarsening.zero_packet_component
77 #print axioms KomorebiPaperVI.Coarsening.zero_packet_weighted
78 #print axioms KomorebiPaperVI.Coarsening.effective_weight
79 #print axioms KomorebiPaperVI.Coarsening.effective_nonnegative
80 #print axioms KomorebiPaperVI.Coarsening.effective_evidence
81 #print axioms KomorebiPaperVI.Coarsening.effective_factorization
82 #print axioms KomorebiPaperVI.Coarsening.packet_reconstruction_point
83 #print axioms KomorebiPaperVI.Coarsening.packet_reconstruction
84 #print axioms KomorebiPaperVI.Coarsening.blockwise_weight
85 #print axioms KomorebiPaperVI.Coarsening.blockwise_evidence
86 #print axioms KomorebiPaperVI.Coarsening.blockwise_sufficiency
87 #print axioms KomorebiPaperVI.Coarsening.scaled_blockwise_sufficiency
88 #print axioms KomorebiPaperVI.Coarsening.one_packet_posterior
89 #print axioms KomorebiPaperVI.Profiles.profile_equivalence
90 #print axioms KomorebiPaperVI.Profiles.likelihood_resolving_iff_refines
91 #print axioms KomorebiPaperVI.Profiles.exact_profile_factorization
92 #print axioms KomorebiPaperVI.ComplexMemory.damped_eq_shifted
93 #print axioms KomorebiPaperVI.ComplexMemory.shifted_decay
94 #print axioms KomorebiPaperVI.ComplexMemory.integral_transfer_right
95 #print axioms KomorebiPaperVI.ComplexMemory.laplace_inverse
96 #print axioms KomorebiPaperVI.ComplexMemory.memory_self_energy
97 #print axioms KomorebiPaperVI.ComplexMemory.normal_growth
98 #print axioms KomorebiPaperVI.ComplexMemory.normal_memory_self_energy
99 #print axioms KomorebiPaperVI.ComplexSemigroups.duhamel_integrand_derivative
100 #print axioms KomorebiPaperVI.ComplexSemigroups.duhamel_rectangular
101 #print axioms KomorebiPaperVI.ComplexSemigroups.exact_rectangular_intertwining
102 #print axioms KomorebiPaperVI.ComplexSemigroups.contraction_duhamel_bound
103 #print axioms KomorebiPaperVI.ConditionalExpectation.fiber_mass_cast
104 #print axioms KomorebiPaperVI.ConditionalExpectation.fiber_pull
105 #print axioms KomorebiPaperVI.ConditionalExpectation.fiber_mass_ne
106 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_constant
107 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_block_constant
108 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_idempotent
109 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_fixes_iff
110 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_range
111 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_matrix
112 #print axioms KomorebiPaperVI.ConditionalExpectation.kernel_weighted_symmetry
113 #print axioms KomorebiPaperVI.ConditionalExpectation.expect_self_adjoint
114 #print axioms KomorebiPaperVI.ConditionalTowers.weighted_inner_separates
115 #print axioms KomorebiPaperVI.ConditionalTowers.fine_after_coarse
116 #print axioms KomorebiPaperVI.ConditionalTowers.coarse_after_fine
117 #print axioms KomorebiPaperVI.ConditionalTowers.conditional_kernel_product
118 #print axioms KomorebiPaperVI.ConditionalTowers.nested_kernel_min
119 #print axioms KomorebiPaperVI.ConditionalTowers.martingale_packet_product
120 #print axioms KomorebiPaperVI.ConditionalTowers.martingale_packet_reconstruction
121 #print axioms KomorebiPaperVI.ContourNaturality.circle_mul_left
122 #print axioms KomorebiPaperVI.ContourNaturality.circle_mul_right
123 #print axioms KomorebiPaperVI.ContourNaturality.resolvent_intertwines
124 #print axioms KomorebiPaperVI.ContourNaturality.common_contour_naturality
125 #print axioms KomorebiPaperVI.DiscreteGreen.green_zero
126 #print axioms KomorebiPaperVI.DiscreteGreen.green_end
127 #print axioms KomorebiPaperVI.DiscreteGreen.green_second_difference
128 #print axioms KomorebiPaperVI.DiscreteGreen.sparse_sum
129 #print axioms KomorebiPaperVI.DiscreteGreen.tridiagonal_mul
130 #print axioms KomorebiPaperVI.DiscreteGreen.tridiagonal_inverse_kernel
131 #print axioms KomorebiPaperVI.DiscreteGreen.inverse_eq_kernel
132 #print axioms KomorebiPaperVI.DiscreteGreen.laplacian_inverse
133 #print axioms KomorebiPaperVI.DiscreteGreen.grid_reconstruction
134 #print axioms KomorebiPaperVI.FeynmanKac.sum_paths_succ
135 #print axioms KomorebiPaperVI.FeynmanKac.transfer_entry
136 #print axioms KomorebiPaperVI.FeynmanKac.path_probability_nonnegative
137 #print axioms KomorebiPaperVI.FeynmanKac.path_probability_mass
138 #print axioms KomorebiPaperVI.FeynmanKac.path_expectation_zero
139 #print axioms KomorebiPaperVI.FeynmanKac.path_expectation_step
140 #print axioms KomorebiPaperVI.FeynmanKac.feynman_kac_path_formula
141 #print axioms KomorebiPaperVI.FeynmanKac.path_probability_product
142 #print axioms KomorebiPaperVI.FeynmanKac.path_potential_sum
143 #print axioms KomorebiPaperVI.FeynmanKac.terminal_last
144 #print axioms KomorebiPaperVI.FiniteBayes.normalized_mass
145 #print axioms KomorebiPaperVI.FiniteBayes.posterior_mass
146 #print axioms KomorebiPaperVI.FiniteBayes.posterior_nonnegative
147 #print axioms KomorebiPaperVI.FiniteBayes.evidence_scale
148 #print axioms KomorebiPaperVI.FiniteBayes.posterior_scale
149 #print axioms KomorebiPaperVI.FiniteBayes.sequential_evidence
150 #print axioms KomorebiPaperVI.FiniteBayes.posterior_composition
151 #print axioms KomorebiPaperVI.FiniteBayes.posterior_difference
152 #print axioms KomorebiPaperVI.FiniteBayes.scale_null_direction
153 #print axioms KomorebiPaperVI.FiniteBayes.normalized_l1_bound_left
154 #print axioms KomorebiPaperVI.FiniteBayes.likelihood_perturbation_bound
155 #print axioms KomorebiPaperVI.FiniteBayes.posterior_probability
156 #print axioms KomorebiPaperVI.FiniteBayes.prediction_probability
157 #print axioms KomorebiPaperVI.FiniteBayes.prediction_update_probability
158 #print axioms KomorebiPaperVI.FractionalIntegral.common_measure_defect
159 #print axioms KomorebiPaperVI.FractionalIntegral.scalar_normalizer_positive
160 #print axioms KomorebiPaperVI.FractionalIntegral.scalar_normalized_representation
161 #print axioms KomorebiPaperVI.FractionalNormBounds.integrand_saturation
162 #print axioms KomorebiPaperVI.FractionalNormBounds.integrand_low_bound
163 #print axioms KomorebiPaperVI.FractionalNormBounds.integrand_gap_bound
164 #print axioms KomorebiPaperVI.FractionalNormBounds.integrand_high_bound
165 #print axioms KomorebiPaperVI.FractionalNormBounds.common_gap_estimate
166 #print axioms KomorebiPaperVI.FractionalNormBounds.holder_estimate
167 #print axioms KomorebiPaperVI.FractionalResolvent.cfc_integrand
168 #print axioms KomorebiPaperVI.FractionalResolvent.integrand_defect
169 #print axioms KomorebiPaperVI.FractionalResolvent.normalized_defect
170 #print axioms KomorebiPaperVI.FractionalResolvent.exact_fractional_intertwining
171 #print axioms KomorebiPaperVI.FractionalScalarBounds.low_integral
172 #print axioms KomorebiPaperVI.FractionalScalarBounds.high_integral
173 #print axioms KomorebiPaperVI.FractionalScalarBounds.split_domain
174 #print axioms KomorebiPaperVI.FractionalScalarBounds.split_norm_bound
175 #print axioms KomorebiPaperVI.FractionalScalarBounds.optimize_split
176 #print axioms KomorebiPaperVI.FractionalSemigroup.power_nonnegative
177 #print axioms KomorebiPaperVI.FractionalSemigroup.exponential_cfc
178 #print axioms KomorebiPaperVI.FractionalSemigroup.exponential_contraction
179 #print axioms KomorebiPaperVI.FractionalSemigroup.exponential_gap
180 #print axioms KomorebiPaperVI.FractionalSemigroup.evolution_transfer
181 #print axioms KomorebiPaperVI.FractionalSemigroup.fractional_duhamel
182 #print axioms KomorebiPaperVI.FractionalSemigroup.fractional_contraction_bound
183 #print axioms KomorebiPaperVI.FractionalSemigroup.fractional_gap_bound
184 #print axioms KomorebiPaperVI.FractionalTowers.bounded_time_majorant
185 #print axioms KomorebiPaperVI.FractionalTowers.time_defects_norm_summable
186 #print axioms KomorebiPaperVI.FractionalTowers.time_defects_summable
187 #print axioms KomorebiPaperVI.FractionalTowers.bounded_time_uniform_convergence
188 #print axioms KomorebiPaperVI.HolomorphicContours.resolvent_continuousAt
189 #print axioms KomorebiPaperVI.HolomorphicContours.holomorphic_circle_integrable
190 #print axioms KomorebiPaperVI.HolomorphicContours.holomorphic_common_contour_naturality
191 #print axioms KomorebiPaperVI.HolomorphicFinite.canonical_unique
192 #print axioms KomorebiPaperVI.HolomorphicFinite.holomorphic_on_component
193 #print axioms KomorebiPaperVI.HolomorphicFinite.component_mem_spectrum
194 #print axioms KomorebiPaperVI.HolomorphicFinite.calculus_spectrum_congr
195 #print axioms KomorebiPaperVI.HolomorphicFinite.cauchyCoefficient_eq
196 #print axioms KomorebiPaperVI.HolomorphicFinite.cauchyCoefficient_independent
197 #print axioms KomorebiPaperVI.HolomorphicFinite.admissible_circle
198 #print axioms KomorebiPaperVI.HolomorphicFinite.canonical_cauchy_representation
199 #print axioms KomorebiPaperVI.HolomorphicFinite.canonical_contours_exist
200 #print axioms KomorebiPaperVI.HolomorphicFinite.canonical_contours_independent
201 #print axioms KomorebiPaperVI.HolomorphicFinite.matrix_holomorphic_naturality
202 #print axioms KomorebiPaperVI.InformationLoss.lossMatrix_apply
203 #print axioms KomorebiPaperVI.InformationLoss.information_loss_matrix
204 #print axioms KomorebiPaperVI.InformationLoss.information_loss_null
205 #print axioms KomorebiPaperVI.InformationLoss.fiber_loss_bound
206 #print axioms KomorebiPaperVI.InformationLoss.total_loss_bound
207 #print axioms KomorebiPaperVI.InformationLoss.information_loss_norm
208 #print axioms KomorebiPaperVI.LowModeConvergence.sine_square_error
209 #print axioms KomorebiPaperVI.LowModeConvergence.low_mode_error
210 #print axioms KomorebiPaperVI.MarkovSemigroup.matrix_powers_nonnegative
211 #print axioms KomorebiPaperVI.MarkovSemigroup.exponential_nonnegative
212 #print axioms KomorebiPaperVI.MarkovSemigroup.shifted_generator_nonnegative
213 #print axioms KomorebiPaperVI.MarkovSemigroup.scalar_exponential
214 #print axioms KomorebiPaperVI.MarkovSemigroup.markov_nonnegative
215 #print axioms KomorebiPaperVI.MarkovSemigroup.generator_power_columns
216 #print axioms KomorebiPaperVI.MarkovSemigroup.markov_column_sum
217 #print axioms KomorebiPaperVI.MarkovSemigroup.markov_probability
218 #print axioms KomorebiPaperVI.MartingalePackets.packet_product
219 #print axioms KomorebiPaperVI.MartingalePackets.packet_sum
220 #print axioms KomorebiPaperVI.MatrixMemory.rectangular_memory_self_energy
221 #print axioms KomorebiPaperVI.MemoryLaplace.decay_integrable
222 #print axioms KomorebiPaperVI.MemoryLaplace.decay_tendsto_zero
223 #print axioms KomorebiPaperVI.MemoryLaplace.integral_generator_transfer
224 #print axioms KomorebiPaperVI.MemoryLaplace.shifted_laplace_right_inverse
225 #print axioms KomorebiPaperVI.MemoryLaplace.memory_integral
226 #print axioms KomorebiPaperVI.NonnormalMemory.left_shift_power
227 #print axioms KomorebiPaperVI.NonnormalMemory.component_spectrum
228 #print axioms KomorebiPaperVI.NonnormalMemory.exp_mul_component
229 #print axioms KomorebiPaperVI.NonnormalMemory.damped_mul_component
230 #print axioms KomorebiPaperVI.NonnormalMemory.component_decay
231 #print axioms KomorebiPaperVI.NonnormalMemory.spectral_decay
232 #print axioms KomorebiPaperVI.NonnormalMemory.spectral_laplace_inverse
233 #print axioms KomorebiPaperVI.NonnormalMemory.nonnormal_self_energy
234 #print axioms KomorebiPaperVI.NormalizedFractional.scalar_measure
235 #print axioms KomorebiPaperVI.NormalizedFractional.cfc_explicit_measure
236 #print axioms KomorebiPaperVI.NormalizedFractional.cfc_lebesgue_integral
237 #print axioms KomorebiPaperVI.OperatorBounds.growth_duhamel_bound
238 #print axioms KomorebiPaperVI.OperatorBounds.contraction_powers
239 #print axioms KomorebiPaperVI.OperatorBounds.finite_horizon_contraction
240 #print axioms KomorebiPaperVI.PoissonKernel.inverse_half_square
241 #print axioms KomorebiPaperVI.PoissonKernel.kernel_substitution
242 #print axioms KomorebiPaperVI.PoissonKernel.kernel_integrable
243 #print axioms KomorebiPaperVI.PoissonKernel.kernel_mass
244 #print axioms KomorebiPaperVI.PoissonKernel.kernel_nonnegative
245 #print axioms KomorebiPaperVI.PoissonKernel.heat_integrand_bounds
246 #print axioms KomorebiPaperVI.PoissonKernel.heat_integrand_integrable
247 #print axioms KomorebiPaperVI.PoissonKernel.zero_mode_subordination
248 #print axioms KomorebiPaperVI.PoissonKernel.finite_spectral_integrable
249 #print axioms KomorebiPaperVI.PoissonSubordination.scaled_reciprocal_gaussian
250 #print axioms KomorebiPaperVI.PoissonSubordination.heat_substitution
251 #print axioms KomorebiPaperVI.PoissonSubordination.scalar_subordination
252 #print axioms KomorebiPaperVI.PoissonSubordination.finite_spectral_subordination
253 #print axioms KomorebiPaperVI.PoissonSubordination.operator_integrand
254 #print axioms KomorebiPaperVI.PoissonSubordination.operator_subordination
255 #print axioms KomorebiPaperVI.PositiveResolvent.spectral_positive
256 #print axioms KomorebiPaperVI.PositiveResolvent.resolvent_inverse
257 #print axioms KomorebiPaperVI.PositiveResolvent.resolvent_left_inverse
258 #print axioms KomorebiPaperVI.PositiveResolvent.resolvent_right_inverse
259 #print axioms KomorebiPaperVI.PositiveResolvent.resolvent_gap_norm
260 #print axioms KomorebiPaperVI.PositiveResolvent.resolvent_norm
261 #print axioms KomorebiPaperVI.PositiveResolvent.resolvent_defect
262 #print axioms KomorebiPaperVI.PositiveResolvent.saturation_cfc
263 #print axioms KomorebiPaperVI.PositiveResolvent.saturation_norm
264 #print axioms KomorebiPaperVI.ReciprocalGaussian.phi_derivative
265 #print axioms KomorebiPaperVI.ReciprocalGaussian.phi_injective
266 #print axioms KomorebiPaperVI.ReciprocalGaussian.phi_surjective
267 #print axioms KomorebiPaperVI.ReciprocalGaussian.gaussian_jacobian_integrable
268 #print axioms KomorebiPaperVI.ReciprocalGaussian.gaussian_jacobian_integral
269 #print axioms KomorebiPaperVI.ReciprocalGaussian.reciprocal_derivative
270 #print axioms KomorebiPaperVI.ReciprocalGaussian.reciprocal_image
271 #print axioms KomorebiPaperVI.ReciprocalGaussian.reciprocal_injective
272 #print axioms KomorebiPaperVI.ReciprocalGaussian.reciprocal_phi
273 #print axioms KomorebiPaperVI.ReciprocalGaussian.reciprocal_gaussian_symmetry
274 #print axioms KomorebiPaperVI.ReciprocalGaussian.phi_gaussian_integrable
275 #print axioms KomorebiPaperVI.ReciprocalGaussian.phi_gaussian_integral
276 #print axioms KomorebiPaperVI.ReciprocalGaussian.reciprocal_square_gaussian
277 #print axioms KomorebiPaperVI.RectangularFractional.normalized_integral
278 #print axioms KomorebiPaperVI.RectangularFractional.low_bound
279 #print axioms KomorebiPaperVI.RectangularFractional.resolvent_defect
280 #print axioms KomorebiPaperVI.RectangularFractional.literal_integrand
281 #print axioms KomorebiPaperVI.RectangularFractional.literal_resolvent_integral
282 #print axioms KomorebiPaperVI.RectangularFractional.exact_fractional_intertwining
283 #print axioms KomorebiPaperVI.RectangularFractional.gap_bound
284 #print axioms KomorebiPaperVI.RectangularFractional.high_bound
285 #print axioms KomorebiPaperVI.RectangularFractional.common_gap_estimate
286 #print axioms KomorebiPaperVI.RectangularFractional.holder_estimate
287 #print axioms KomorebiPaperVI.RectangularSemigroup.evolution_exponential
288 #print axioms KomorebiPaperVI.RectangularSemigroup.evolution_cfc
289 #print axioms KomorebiPaperVI.RectangularSemigroup.contraction
290 #print axioms KomorebiPaperVI.RectangularSemigroup.gap_decay
291 #print axioms KomorebiPaperVI.RectangularSemigroup.fractional_duhamel
292 #print axioms KomorebiPaperVI.RectangularSemigroup.fractional_contraction_bound
293 #print axioms KomorebiPaperVI.RectangularSemigroup.fractional_gap_bound
294 #print axioms KomorebiPaperVI.RectangularSemigroup.generator_gap_bound
295 #print axioms KomorebiPaperVI.RectangularTowers.holder_constant_positive
296 #print axioms KomorebiPaperVI.RectangularTowers.holder_majorant
297 #print axioms KomorebiPaperVI.RectangularTowers.generator_holder_summable
298 #print axioms KomorebiPaperVI.RectangularTowers.generator_gap_summable
299 #print axioms KomorebiPaperVI.RectangularTowers.bounded_time_majorant
300 #print axioms KomorebiPaperVI.RectangularTowers.time_norms_summable
301 #print axioms KomorebiPaperVI.RectangularTowers.bounded_time_uniform_convergence
302 #print axioms KomorebiPaperVI.RectangularTowers.holder_tower
303 #print axioms KomorebiPaperVI.RectangularTowers.gap_tower
304 #print axioms KomorebiPaperVI.ReducingPackets.generator_commutes
305 #print axioms KomorebiPaperVI.ReducingPackets.reducing_exponential
306 #print axioms KomorebiPaperVI.ReducingPackets.compressed_evolution
307 #print axioms KomorebiPaperVI.ScalarDecay.norm_exp_pow
308 #print axioms KomorebiPaperVI.ScalarDecay.exp_pow_integrable
309 #print axioms KomorebiPaperVI.ScalarDecay.exp_pow_tendsto_zero
310 #print axioms KomorebiPaperVI.SchurFeshbach.resolvent_blocks
311 #print axioms KomorebiPaperVI.SchurFeshbach.projected_resolvent
312 #print axioms KomorebiPaperVI.SchurFeshbach.schur_invertible
313 #print axioms KomorebiPaperVI.Semigroups.transfer_zero
314 #print axioms KomorebiPaperVI.Semigroups.transfer_add
315 #print axioms KomorebiPaperVI.Semigroups.transfer_derivative_right
316 #print axioms KomorebiPaperVI.Semigroups.transfer_derivative_left
317 #print axioms KomorebiPaperVI.Semigroups.transfer_continuous
318 #print axioms KomorebiPaperVI.Semigroups.transfer_intertwining
319 #print axioms KomorebiPaperVI.Semigroups.exponential_packet_convolution
320 #print axioms KomorebiPaperVI.Semigroups.duhamel_integrand_derivative
321 #print axioms KomorebiPaperVI.Semigroups.duhamel_rectangular
322 #print axioms KomorebiPaperVI.Semigroups.exact_rectangular_intertwining
323 #print axioms KomorebiPaperVI.Semigroups.contraction_duhamel_bound
324 #print axioms KomorebiPaperVI.SpectralPackets.resolve_mul
325 #print axioms KomorebiPaperVI.SpectralPackets.resolve_left_packet
326 #print axioms KomorebiPaperVI.SpectralPackets.resolve_right_packet
327 #print axioms KomorebiPaperVI.SpectralPackets.exp_resolution
328 #print axioms KomorebiPaperVI.SpectralPackets.fractional_add
329 #print axioms KomorebiPaperVI.SpectralPackets.spectral_transfer_exponential
330 #print axioms KomorebiPaperVI.SpectralPackets.spectral_transfer_add
331 #print axioms KomorebiPaperVI.SpectralPackets.fractional_reduces
332 #print axioms KomorebiPaperVI.SpectralPackets.spectral_transfer_reduces
333 #print axioms KomorebiPaperVI.Survival.survival_zero
334 #print axioms KomorebiPaperVI.Survival.state_nonnegative
335 #print axioms KomorebiPaperVI.Survival.survival_positive
336 #print axioms KomorebiPaperVI.Survival.density_nonnegative
337 #print axioms KomorebiPaperVI.Survival.survival_derivative
338 #print axioms KomorebiPaperVI.Survival.survival_antitone
339 #print axioms KomorebiPaperVI.Survival.density_continuous
340 #print axioms KomorebiPaperVI.Survival.survival_hazard
341 #print axioms KomorebiPaperVI.Survival.survival_has_limit
342 #print axioms KomorebiPaperVI.Survival.defective_density_mass
343 #print axioms KomorebiPaperVI.Survival.eventual_absorption_density
344 
345 open Lean Meta Elab Command
346 
347 run_cmd do
348   let env ← getEnv
349   let targets : Array Name := #[
350     `KomorebiPaperVI.Algebra.block_reconstruction,
351     `KomorebiPaperVI.Algebra.block_multiplication,
352     `KomorebiPaperVI.Algebra.packet_semigroup_convolution,
353     `KomorebiPaperVI.Algebra.difference_idempotent,
354     `KomorebiPaperVI.Algebra.difference_annihilates_coarse,
355     `KomorebiPaperVI.Algebra.tower_telescope,
356     `KomorebiPaperVI.Algebra.intertwining_powers,
357     `KomorebiPaperVI.Algebra.finite_horizon_defect,
358     `KomorebiPaperVI.Algebra.rectangular_resolvent_identity,
359     `KomorebiPaperVI.BanachDefects.duhamel_derivative,
360     `KomorebiPaperVI.BanachDefects.duhamel,
361     `KomorebiPaperVI.BanachDefects.contraction_bound,
362     `KomorebiPaperVI.BayesianFlow.positive_evidence,
363     `KomorebiPaperVI.BayesianFlow.flow_probability,
364     `KomorebiPaperVI.BayesianFlow.likelihood_add,
365     `KomorebiPaperVI.BayesianFlow.flow_add,
366     `KomorebiPaperVI.BayesianFlow.flow_zero,
367     `KomorebiPaperVI.BayesianFlow.likelihood_derivative,
368     `KomorebiPaperVI.BayesianFlow.evidence_derivative,
369     `KomorebiPaperVI.BayesianFlow.flow_derivative,
370     `KomorebiPaperVI.BayesianNecessity.pair_weighted_sum,
371     `KomorebiPaperVI.BayesianNecessity.pair_probability,
372     `KomorebiPaperVI.BayesianNecessity.pair_fiber_weight,
373     `KomorebiPaperVI.BayesianNecessity.pair_coarsen,
374     `KomorebiPaperVI.BayesianNecessity.pair_coarse_posterior,
375     `KomorebiPaperVI.BayesianNecessity.cross_packet_ratio,
376     `KomorebiPaperVI.BayesianNecessity.all_packet_ratio,
377     `KomorebiPaperVI.BayesianNecessity.positive_evidence,
378     `KomorebiPaperVI.BayesianNecessity.refinement_iff,
379     `KomorebiPaperVI.BayesianPartitions.packetMap_surjective,
380     `KomorebiPaperVI.BayesianPartitions.packetLikelihood_apply,
381     `KomorebiPaperVI.BayesianPartitions.packet_eq_iff,
382     `KomorebiPaperVI.BayesianPartitions.packetLikelihood_positive,
383     `KomorebiPaperVI.BayesianPartitions.canonical_coarsening,
384     `KomorebiPaperVI.BayesianPartitions.canonical_unique_factor,
385     `KomorebiPaperVI.BayesianPartitions.all_prior_family_iff_resolves,
386     `KomorebiPaperVI.BayesianPartitions.canonical_coarsest_nontrivial,
387     `KomorebiPaperVI.BayesianPartitions.canonical_nontrivial,
388     `KomorebiPaperVI.BayesianTowers.coarsen_comp,
389     `KomorebiPaperVI.BayesianTowers.singleton_commutes,
390     `KomorebiPaperVI.BayesianTowers.adjacent_criterion,
391     `KomorebiPaperVI.BayesianTowers.compose_commutes,
392     `KomorebiPaperVI.BayesianTowers.coarsen_id,
393     `KomorebiPaperVI.BayesianTowers.tower_commutes,
394     `KomorebiPaperVI.BayesianTowers.tower_criterion,
395     `KomorebiPaperVI.BetaNormalization.beta_value,
396     `KomorebiPaperVI.BetaNormalization.change_derivative,
397     `KomorebiPaperVI.BetaNormalization.change_injective,
398     `KomorebiPaperVI.BetaNormalization.change_image,
399     `KomorebiPaperVI.BetaNormalization.change_integrand,
400     `KomorebiPaperVI.BetaNormalization.rational_integral,
401     `KomorebiPaperVI.BetaNormalization.normalizer_exact,
402     `KomorebiPaperVI.BetaNormalization.sine_factor_positive,
403     `KomorebiPaperVI.BetaNormalization.scalar_fractional_integral,
404     `KomorebiPaperVI.BetaNormalization.beta_real_integral,
405     `KomorebiPaperVI.BetaNormalization.weighted_beta_value,
406     `KomorebiPaperVI.BetaNormalization.gap_change_integrand,
407     `KomorebiPaperVI.BetaNormalization.unit_gap_integral,
408     `KomorebiPaperVI.BetaNormalization.gap_integral,
409     `KomorebiPaperVI.BetaNormalization.normalized_gap_integral,
410     `KomorebiPaperVI.CanonicalJets.calculus_on_component,
411     `KomorebiPaperVI.CanonicalJets.power_kills,
412     `KomorebiPaperVI.CanonicalJets.jet_stable,
413     `KomorebiPaperVI.CanonicalJets.shift_intertwines,
414     `KomorebiPaperVI.CanonicalJets.power_intertwines,
415     `KomorebiPaperVI.CanonicalJets.jet_intertwines,
416     `KomorebiPaperVI.CanonicalJets.canonical_naturality,
417     `KomorebiPaperVI.CanonicalJets.holomorphic_naturality,
418     `KomorebiPaperVI.Coarsening.coarsen_mass,
419     `KomorebiPaperVI.Coarsening.coarsen_nonnegative,
420     `KomorebiPaperVI.Coarsening.coarsen_probability,
421     `KomorebiPaperVI.Coarsening.coarsen_div,
422     `KomorebiPaperVI.Coarsening.coarsen_posterior,
423     `KomorebiPaperVI.Coarsening.zero_packet_component,
424     `KomorebiPaperVI.Coarsening.zero_packet_weighted,
425     `KomorebiPaperVI.Coarsening.effective_weight,
426     `KomorebiPaperVI.Coarsening.effective_nonnegative,
427     `KomorebiPaperVI.Coarsening.effective_evidence,
428     `KomorebiPaperVI.Coarsening.effective_factorization,
429     `KomorebiPaperVI.Coarsening.packet_reconstruction_point,
430     `KomorebiPaperVI.Coarsening.packet_reconstruction,
431     `KomorebiPaperVI.Coarsening.blockwise_weight,
432     `KomorebiPaperVI.Coarsening.blockwise_evidence,
433     `KomorebiPaperVI.Coarsening.blockwise_sufficiency,
434     `KomorebiPaperVI.Coarsening.scaled_blockwise_sufficiency,
435     `KomorebiPaperVI.Coarsening.one_packet_posterior,
436     `KomorebiPaperVI.Profiles.profile_equivalence,
437     `KomorebiPaperVI.Profiles.likelihood_resolving_iff_refines,
438     `KomorebiPaperVI.Profiles.exact_profile_factorization,
439     `KomorebiPaperVI.ComplexMemory.damped_eq_shifted,
440     `KomorebiPaperVI.ComplexMemory.shifted_decay,
441     `KomorebiPaperVI.ComplexMemory.integral_transfer_right,
442     `KomorebiPaperVI.ComplexMemory.laplace_inverse,
443     `KomorebiPaperVI.ComplexMemory.memory_self_energy,
444     `KomorebiPaperVI.ComplexMemory.normal_growth,
445     `KomorebiPaperVI.ComplexMemory.normal_memory_self_energy,
446     `KomorebiPaperVI.ComplexSemigroups.duhamel_integrand_derivative,
447     `KomorebiPaperVI.ComplexSemigroups.duhamel_rectangular,
448     `KomorebiPaperVI.ComplexSemigroups.exact_rectangular_intertwining,
449     `KomorebiPaperVI.ComplexSemigroups.contraction_duhamel_bound,
450     `KomorebiPaperVI.ConditionalExpectation.fiber_mass_cast,
451     `KomorebiPaperVI.ConditionalExpectation.fiber_pull,
452     `KomorebiPaperVI.ConditionalExpectation.fiber_mass_ne,
453     `KomorebiPaperVI.ConditionalExpectation.expect_constant,
454     `KomorebiPaperVI.ConditionalExpectation.expect_block_constant,
455     `KomorebiPaperVI.ConditionalExpectation.expect_idempotent,
456     `KomorebiPaperVI.ConditionalExpectation.expect_fixes_iff,
457     `KomorebiPaperVI.ConditionalExpectation.expect_range,
458     `KomorebiPaperVI.ConditionalExpectation.expect_matrix,
459     `KomorebiPaperVI.ConditionalExpectation.kernel_weighted_symmetry,
460     `KomorebiPaperVI.ConditionalExpectation.expect_self_adjoint,
461     `KomorebiPaperVI.ConditionalTowers.weighted_inner_separates,
462     `KomorebiPaperVI.ConditionalTowers.fine_after_coarse,
463     `KomorebiPaperVI.ConditionalTowers.coarse_after_fine,
464     `KomorebiPaperVI.ConditionalTowers.conditional_kernel_product,
465     `KomorebiPaperVI.ConditionalTowers.nested_kernel_min,
466     `KomorebiPaperVI.ConditionalTowers.martingale_packet_product,
467     `KomorebiPaperVI.ConditionalTowers.martingale_packet_reconstruction,
468     `KomorebiPaperVI.ContourNaturality.circle_mul_left,
469     `KomorebiPaperVI.ContourNaturality.circle_mul_right,
470     `KomorebiPaperVI.ContourNaturality.resolvent_intertwines,
471     `KomorebiPaperVI.ContourNaturality.common_contour_naturality,
472     `KomorebiPaperVI.DiscreteGreen.green_zero,
473     `KomorebiPaperVI.DiscreteGreen.green_end,
474     `KomorebiPaperVI.DiscreteGreen.green_second_difference,
475     `KomorebiPaperVI.DiscreteGreen.sparse_sum,
476     `KomorebiPaperVI.DiscreteGreen.tridiagonal_mul,
477     `KomorebiPaperVI.DiscreteGreen.tridiagonal_inverse_kernel,
478     `KomorebiPaperVI.DiscreteGreen.inverse_eq_kernel,
479     `KomorebiPaperVI.DiscreteGreen.laplacian_inverse,
480     `KomorebiPaperVI.DiscreteGreen.grid_reconstruction,
481     `KomorebiPaperVI.FeynmanKac.sum_paths_succ,
482     `KomorebiPaperVI.FeynmanKac.transfer_entry,
483     `KomorebiPaperVI.FeynmanKac.path_probability_nonnegative,
484     `KomorebiPaperVI.FeynmanKac.path_probability_mass,
485     `KomorebiPaperVI.FeynmanKac.path_expectation_zero,
486     `KomorebiPaperVI.FeynmanKac.path_expectation_step,
487     `KomorebiPaperVI.FeynmanKac.feynman_kac_path_formula,
488     `KomorebiPaperVI.FeynmanKac.path_probability_product,
489     `KomorebiPaperVI.FeynmanKac.path_potential_sum,
490     `KomorebiPaperVI.FeynmanKac.terminal_last,
491     `KomorebiPaperVI.FiniteBayes.normalized_mass,
492     `KomorebiPaperVI.FiniteBayes.posterior_mass,
493     `KomorebiPaperVI.FiniteBayes.posterior_nonnegative,
494     `KomorebiPaperVI.FiniteBayes.evidence_scale,
495     `KomorebiPaperVI.FiniteBayes.posterior_scale,
496     `KomorebiPaperVI.FiniteBayes.sequential_evidence,
497     `KomorebiPaperVI.FiniteBayes.posterior_composition,
498     `KomorebiPaperVI.FiniteBayes.posterior_difference,
499     `KomorebiPaperVI.FiniteBayes.scale_null_direction,
500     `KomorebiPaperVI.FiniteBayes.normalized_l1_bound_left,
501     `KomorebiPaperVI.FiniteBayes.likelihood_perturbation_bound,
502     `KomorebiPaperVI.FiniteBayes.posterior_probability,
503     `KomorebiPaperVI.FiniteBayes.prediction_probability,
504     `KomorebiPaperVI.FiniteBayes.prediction_update_probability,
505     `KomorebiPaperVI.FractionalIntegral.common_measure_defect,
506     `KomorebiPaperVI.FractionalIntegral.scalar_normalizer_positive,
507     `KomorebiPaperVI.FractionalIntegral.scalar_normalized_representation,
508     `KomorebiPaperVI.FractionalNormBounds.integrand_saturation,
509     `KomorebiPaperVI.FractionalNormBounds.integrand_low_bound,
510     `KomorebiPaperVI.FractionalNormBounds.integrand_gap_bound,
511     `KomorebiPaperVI.FractionalNormBounds.integrand_high_bound,
512     `KomorebiPaperVI.FractionalNormBounds.common_gap_estimate,
513     `KomorebiPaperVI.FractionalNormBounds.holder_estimate,
514     `KomorebiPaperVI.FractionalResolvent.cfc_integrand,
515     `KomorebiPaperVI.FractionalResolvent.integrand_defect,
516     `KomorebiPaperVI.FractionalResolvent.normalized_defect,
517     `KomorebiPaperVI.FractionalResolvent.exact_fractional_intertwining,
518     `KomorebiPaperVI.FractionalScalarBounds.low_integral,
519     `KomorebiPaperVI.FractionalScalarBounds.high_integral,
520     `KomorebiPaperVI.FractionalScalarBounds.split_domain,
521     `KomorebiPaperVI.FractionalScalarBounds.split_norm_bound,
522     `KomorebiPaperVI.FractionalScalarBounds.optimize_split,
523     `KomorebiPaperVI.FractionalSemigroup.power_nonnegative,
524     `KomorebiPaperVI.FractionalSemigroup.exponential_cfc,
525     `KomorebiPaperVI.FractionalSemigroup.exponential_contraction,
526     `KomorebiPaperVI.FractionalSemigroup.exponential_gap,
527     `KomorebiPaperVI.FractionalSemigroup.evolution_transfer,
528     `KomorebiPaperVI.FractionalSemigroup.fractional_duhamel,
529     `KomorebiPaperVI.FractionalSemigroup.fractional_contraction_bound,
530     `KomorebiPaperVI.FractionalSemigroup.fractional_gap_bound,
531     `KomorebiPaperVI.FractionalTowers.bounded_time_majorant,
532     `KomorebiPaperVI.FractionalTowers.time_defects_norm_summable,
533     `KomorebiPaperVI.FractionalTowers.time_defects_summable,
534     `KomorebiPaperVI.FractionalTowers.bounded_time_uniform_convergence,
535     `KomorebiPaperVI.HolomorphicContours.resolvent_continuousAt,
536     `KomorebiPaperVI.HolomorphicContours.holomorphic_circle_integrable,
537     `KomorebiPaperVI.HolomorphicContours.holomorphic_common_contour_naturality,
538     `KomorebiPaperVI.HolomorphicFinite.canonical_unique,
539     `KomorebiPaperVI.HolomorphicFinite.holomorphic_on_component,
540     `KomorebiPaperVI.HolomorphicFinite.component_mem_spectrum,
541     `KomorebiPaperVI.HolomorphicFinite.calculus_spectrum_congr,
542     `KomorebiPaperVI.HolomorphicFinite.cauchyCoefficient_eq,
543     `KomorebiPaperVI.HolomorphicFinite.cauchyCoefficient_independent,
544     `KomorebiPaperVI.HolomorphicFinite.admissible_circle,
545     `KomorebiPaperVI.HolomorphicFinite.canonical_cauchy_representation,
546     `KomorebiPaperVI.HolomorphicFinite.canonical_contours_exist,
547     `KomorebiPaperVI.HolomorphicFinite.canonical_contours_independent,
548     `KomorebiPaperVI.HolomorphicFinite.matrix_holomorphic_naturality,
549     `KomorebiPaperVI.InformationLoss.lossMatrix_apply,
550     `KomorebiPaperVI.InformationLoss.information_loss_matrix,
551     `KomorebiPaperVI.InformationLoss.information_loss_null,
552     `KomorebiPaperVI.InformationLoss.fiber_loss_bound,
553     `KomorebiPaperVI.InformationLoss.total_loss_bound,
554     `KomorebiPaperVI.InformationLoss.information_loss_norm,
555     `KomorebiPaperVI.LowModeConvergence.sine_square_error,
556     `KomorebiPaperVI.LowModeConvergence.low_mode_error,
557     `KomorebiPaperVI.MarkovSemigroup.matrix_powers_nonnegative,
558     `KomorebiPaperVI.MarkovSemigroup.exponential_nonnegative,
559     `KomorebiPaperVI.MarkovSemigroup.shifted_generator_nonnegative,
560     `KomorebiPaperVI.MarkovSemigroup.scalar_exponential,
561     `KomorebiPaperVI.MarkovSemigroup.markov_nonnegative,
562     `KomorebiPaperVI.MarkovSemigroup.generator_power_columns,
563     `KomorebiPaperVI.MarkovSemigroup.markov_column_sum,
564     `KomorebiPaperVI.MarkovSemigroup.markov_probability,
565     `KomorebiPaperVI.MartingalePackets.packet_product,
566     `KomorebiPaperVI.MartingalePackets.packet_sum,
567     `KomorebiPaperVI.MatrixMemory.rectangular_memory_self_energy,
568     `KomorebiPaperVI.MemoryLaplace.decay_integrable,
569     `KomorebiPaperVI.MemoryLaplace.decay_tendsto_zero,
570     `KomorebiPaperVI.MemoryLaplace.integral_generator_transfer,
571     `KomorebiPaperVI.MemoryLaplace.shifted_laplace_right_inverse,
572     `KomorebiPaperVI.MemoryLaplace.memory_integral,
573     `KomorebiPaperVI.NonnormalMemory.left_shift_power,
574     `KomorebiPaperVI.NonnormalMemory.component_spectrum,
575     `KomorebiPaperVI.NonnormalMemory.exp_mul_component,
576     `KomorebiPaperVI.NonnormalMemory.damped_mul_component,
577     `KomorebiPaperVI.NonnormalMemory.component_decay,
578     `KomorebiPaperVI.NonnormalMemory.spectral_decay,
579     `KomorebiPaperVI.NonnormalMemory.spectral_laplace_inverse,
580     `KomorebiPaperVI.NonnormalMemory.nonnormal_self_energy,
581     `KomorebiPaperVI.NormalizedFractional.scalar_measure,
582     `KomorebiPaperVI.NormalizedFractional.cfc_explicit_measure,
583     `KomorebiPaperVI.NormalizedFractional.cfc_lebesgue_integral,
584     `KomorebiPaperVI.OperatorBounds.growth_duhamel_bound,
585     `KomorebiPaperVI.OperatorBounds.contraction_powers,
586     `KomorebiPaperVI.OperatorBounds.finite_horizon_contraction,
587     `KomorebiPaperVI.PoissonKernel.inverse_half_square,
588     `KomorebiPaperVI.PoissonKernel.kernel_substitution,
589     `KomorebiPaperVI.PoissonKernel.kernel_integrable,
590     `KomorebiPaperVI.PoissonKernel.kernel_mass,
591     `KomorebiPaperVI.PoissonKernel.kernel_nonnegative,
592     `KomorebiPaperVI.PoissonKernel.heat_integrand_bounds,
593     `KomorebiPaperVI.PoissonKernel.heat_integrand_integrable,
594     `KomorebiPaperVI.PoissonKernel.zero_mode_subordination,
595     `KomorebiPaperVI.PoissonKernel.finite_spectral_integrable,
596     `KomorebiPaperVI.PoissonSubordination.scaled_reciprocal_gaussian,
597     `KomorebiPaperVI.PoissonSubordination.heat_substitution,
598     `KomorebiPaperVI.PoissonSubordination.scalar_subordination,
599     `KomorebiPaperVI.PoissonSubordination.finite_spectral_subordination,
600     `KomorebiPaperVI.PoissonSubordination.operator_integrand,
601     `KomorebiPaperVI.PoissonSubordination.operator_subordination,
602     `KomorebiPaperVI.PositiveResolvent.spectral_positive,
603     `KomorebiPaperVI.PositiveResolvent.resolvent_inverse,
604     `KomorebiPaperVI.PositiveResolvent.resolvent_left_inverse,
605     `KomorebiPaperVI.PositiveResolvent.resolvent_right_inverse,
606     `KomorebiPaperVI.PositiveResolvent.resolvent_gap_norm,
607     `KomorebiPaperVI.PositiveResolvent.resolvent_norm,
608     `KomorebiPaperVI.PositiveResolvent.resolvent_defect,
609     `KomorebiPaperVI.PositiveResolvent.saturation_cfc,
610     `KomorebiPaperVI.PositiveResolvent.saturation_norm,
611     `KomorebiPaperVI.ReciprocalGaussian.phi_derivative,
612     `KomorebiPaperVI.ReciprocalGaussian.phi_injective,
613     `KomorebiPaperVI.ReciprocalGaussian.phi_surjective,
614     `KomorebiPaperVI.ReciprocalGaussian.gaussian_jacobian_integrable,
615     `KomorebiPaperVI.ReciprocalGaussian.gaussian_jacobian_integral,
616     `KomorebiPaperVI.ReciprocalGaussian.reciprocal_derivative,
617     `KomorebiPaperVI.ReciprocalGaussian.reciprocal_image,
618     `KomorebiPaperVI.ReciprocalGaussian.reciprocal_injective,
619     `KomorebiPaperVI.ReciprocalGaussian.reciprocal_phi,
620     `KomorebiPaperVI.ReciprocalGaussian.reciprocal_gaussian_symmetry,
621     `KomorebiPaperVI.ReciprocalGaussian.phi_gaussian_integrable,
622     `KomorebiPaperVI.ReciprocalGaussian.phi_gaussian_integral,
623     `KomorebiPaperVI.ReciprocalGaussian.reciprocal_square_gaussian,
624     `KomorebiPaperVI.RectangularFractional.normalized_integral,
625     `KomorebiPaperVI.RectangularFractional.low_bound,
626     `KomorebiPaperVI.RectangularFractional.resolvent_defect,
627     `KomorebiPaperVI.RectangularFractional.literal_integrand,
628     `KomorebiPaperVI.RectangularFractional.literal_resolvent_integral,
629     `KomorebiPaperVI.RectangularFractional.exact_fractional_intertwining,
630     `KomorebiPaperVI.RectangularFractional.gap_bound,
631     `KomorebiPaperVI.RectangularFractional.high_bound,
632     `KomorebiPaperVI.RectangularFractional.common_gap_estimate,
633     `KomorebiPaperVI.RectangularFractional.holder_estimate,
634     `KomorebiPaperVI.RectangularSemigroup.evolution_exponential,
635     `KomorebiPaperVI.RectangularSemigroup.evolution_cfc,
636     `KomorebiPaperVI.RectangularSemigroup.contraction,
637     `KomorebiPaperVI.RectangularSemigroup.gap_decay,
638     `KomorebiPaperVI.RectangularSemigroup.fractional_duhamel,
639     `KomorebiPaperVI.RectangularSemigroup.fractional_contraction_bound,
640     `KomorebiPaperVI.RectangularSemigroup.fractional_gap_bound,
641     `KomorebiPaperVI.RectangularSemigroup.generator_gap_bound,
642     `KomorebiPaperVI.RectangularTowers.holder_constant_positive,
643     `KomorebiPaperVI.RectangularTowers.holder_majorant,
644     `KomorebiPaperVI.RectangularTowers.generator_holder_summable,
645     `KomorebiPaperVI.RectangularTowers.generator_gap_summable,
646     `KomorebiPaperVI.RectangularTowers.bounded_time_majorant,
647     `KomorebiPaperVI.RectangularTowers.time_norms_summable,
648     `KomorebiPaperVI.RectangularTowers.bounded_time_uniform_convergence,
649     `KomorebiPaperVI.RectangularTowers.holder_tower,
650     `KomorebiPaperVI.RectangularTowers.gap_tower,
651     `KomorebiPaperVI.ReducingPackets.generator_commutes,
652     `KomorebiPaperVI.ReducingPackets.reducing_exponential,
653     `KomorebiPaperVI.ReducingPackets.compressed_evolution,
654     `KomorebiPaperVI.ScalarDecay.norm_exp_pow,
655     `KomorebiPaperVI.ScalarDecay.exp_pow_integrable,
656     `KomorebiPaperVI.ScalarDecay.exp_pow_tendsto_zero,
657     `KomorebiPaperVI.SchurFeshbach.resolvent_blocks,
658     `KomorebiPaperVI.SchurFeshbach.projected_resolvent,
659     `KomorebiPaperVI.SchurFeshbach.schur_invertible,
660     `KomorebiPaperVI.Semigroups.transfer_zero,
661     `KomorebiPaperVI.Semigroups.transfer_add,
662     `KomorebiPaperVI.Semigroups.transfer_derivative_right,
663     `KomorebiPaperVI.Semigroups.transfer_derivative_left,
664     `KomorebiPaperVI.Semigroups.transfer_continuous,
665     `KomorebiPaperVI.Semigroups.transfer_intertwining,
666     `KomorebiPaperVI.Semigroups.exponential_packet_convolution,
667     `KomorebiPaperVI.Semigroups.duhamel_integrand_derivative,
668     `KomorebiPaperVI.Semigroups.duhamel_rectangular,
669     `KomorebiPaperVI.Semigroups.exact_rectangular_intertwining,
670     `KomorebiPaperVI.Semigroups.contraction_duhamel_bound,
671     `KomorebiPaperVI.SpectralPackets.resolve_mul,
672     `KomorebiPaperVI.SpectralPackets.resolve_left_packet,
673     `KomorebiPaperVI.SpectralPackets.resolve_right_packet,
674     `KomorebiPaperVI.SpectralPackets.exp_resolution,
675     `KomorebiPaperVI.SpectralPackets.fractional_add,
676     `KomorebiPaperVI.SpectralPackets.spectral_transfer_exponential,
677     `KomorebiPaperVI.SpectralPackets.spectral_transfer_add,
678     `KomorebiPaperVI.SpectralPackets.fractional_reduces,
679     `KomorebiPaperVI.SpectralPackets.spectral_transfer_reduces,
680     `KomorebiPaperVI.Survival.survival_zero,
681     `KomorebiPaperVI.Survival.state_nonnegative,
682     `KomorebiPaperVI.Survival.survival_positive,
683     `KomorebiPaperVI.Survival.density_nonnegative,
684     `KomorebiPaperVI.Survival.survival_derivative,
685     `KomorebiPaperVI.Survival.survival_antitone,
686     `KomorebiPaperVI.Survival.density_continuous,
687     `KomorebiPaperVI.Survival.survival_hazard,
688     `KomorebiPaperVI.Survival.survival_has_limit,
689     `KomorebiPaperVI.Survival.defective_density_mass,
690     `KomorebiPaperVI.Survival.eventual_absorption_density
691   ]
692   for target in targets do
693     match env.find? target with
694     | some (.thmInfo _) => pure ()
695     | _ => throwError "missing or non-theorem target: {target}"
696   let mut audited : Nat := 0
697   for (name, info) in env.checked.get.constants.toList do
698     if Name.isPrefixOf `KomorebiPaperVI name then
699       audited := audited + 1
700       if info.isUnsafe then
701         throwError "unsafe declaration: {name}"
702       match info with
703       | .axiomInfo _ => throwError "axiom declaration: {name}"
704       | .opaqueInfo _ => throwError "opaque declaration: {name}"
705       | _ => pure ()
706       let axioms ← Lean.collectAxioms name
707       for axiomName in axioms do
708         unless axiomName == ``propext || axiomName == ``Classical.choice ||
709             axiomName == ``Quot.sound do
710           throwError "unexpected axiom {axiomName} in {name}"
711   logInfo m!"PAPER_VI_TARGET_AUDIT_PASS: {targets.size} theorem targets; {audited} namespace declarations"

Back to source controls