OAI/Geometry/TamingCompatibility/Concentration/ActivationMeasureBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.SummableCutoff.activation_boundary_integral line 16
2. lemma OAI.TamingCompatibility.SummableCutoff.activation_error_integral line 36
3. lemma OAI.TamingCompatibility.SummableCutoff.exceptional_null_of_integrals line 51
4. lemma OAI.TamingCompatibility.ManifoldForms.contMDiff_logActivation line 75
5. lemma OAI.TamingCompatibility.ManifoldForms.scalarDifferential_logActivation line 85
6. lemma OAI.TamingCompatibility.ManifoldForms.contMDiff_saturation line 93
7. lemma OAI.TamingCompatibility.ManifoldForms.scalarDifferential_saturation line 100