IndisputableMonolith.NavierStokes.RM2U.NonParasitism

declarations in this module (61)

• structure NonParasitismHypothesis L27
• structure Bet1BoundaryIntegrableHypothesis L44
• theorem nonParasitism_of_bet1 L53
• theorem bet1_boundaryTerm_integrable_of_L2_mul_r L76
• theorem bet1_boundaryTerm_integrable_of_A2r_and_coercive L132
• structure Bet1BoundaryIntegrableHypothesisAlt L153
• theorem bet1_of_bet1Alt L161
• structure Bet2SelfFalsificationHypothesis L214
• def nthPrime L240
• theorem nthPrime_prime L242
• theorem strictMono_nthPrime L246
• theorem pairwise_coprime_nthPrime L249
• structure NonResonantSchedule L261
• def canonical L267
• theorem not_summable_of_uniform_abs_lowerBound L273
• structure PrimeScheduleSelfFalsification L288
• theorem bet2_of_primeSchedule L298
• structure Payments L331
• structure U4PaymentUpperBoundHypothesis L340
• structure C2VanishingInjectionHypothesis L352
• abbrev U4VanishingInjectionRateHypothesis L361
• theorem c2VanishingInjection_comp_two L367
• theorem u4PaymentUpperBound_of_injection L393
• theorem u4PaymentUpperBound_of_u4InjectionRate L450
• structure U4PaymentsControlledByInjectionRateHypothesis L469
• structure U4PayXiControlledByInjectionRateHypothesis L481
• structure U4PayRhoControlledByInjectionRateHypothesis L493
• structure U4BandBudgetControlledByInjectionRateHypothesis L509
• theorem u4PayRhoControlledByInjectionRate_of_bandBudget L525
• structure U4InjectionPaymentPackageHypothesis L615
• theorem u4PaymentUpperBound_of_paymentControl L622
• theorem u4PaymentUpperBound_of_u4Package L634
• structure ForcingToTwistOrBandPaymentHypothesis L708
• structure NoRigidRotationAbsorptionHypothesis L722
• structure NegativeSigmaForcesBandPaymentHypothesis L734
• structure NoPersistentNullAlignmentHypothesis L747
• structure ExportSplitHypothesis L760
• structure ExportForcesPaymentHypothesis L776
• theorem of_split L788
• structure AbsorptionImpliesAffineAnsatzHypothesis L828
• structure AffineAnsatzImpossibleHypothesis L838
• structure TailStrainTimeVariationHypothesis L850
• abbrev TailVorticityL2TimeModulusHypothesis L865
• theorem tailStrainTimeVariation_of_lipschitz L874
• structure AbsorptionClassImpossibleHypothesis L910
• structure ConcavityImpossibleHypothesis L922
• structure U4NoExportHypothesis L933
• theorem of_u4 L950
• structure TailFluxNonVanishImpliesExportAtSmallScales L995
• theorem bet2SelfFalsification_of_u4 L1003
• structure Quasi2DEliminationHypothesis L1020
• structure BackwardUniquenessNSHypothesis L1027
• structure Quasi2DToComparisonSolutionHypothesis L1041
• structure Quasi2DToExactSymmetryHypothesis L1061
• structure SymmetryClassImpossibleHypothesis L1074
• theorem nonParasitism_of_bet2 L1084
• structure Bet3CoerciveL2Hypothesis L1093
• theorem rm2Closed_of_bet3 L1096
• theorem rm2Closed_of_nonParasitism L1108
• theorem rm2Closed_of_bet1 L1116
• theorem rm2Closed_of_bet2 L1123