IndisputableMonolith.Gravity.Analysis.FreudenthalEnergyLimit

declarations in this module (28)

• def witnessField L71
• def sample L75
• def witnessSample L79
• theorem sample_witnessField L82
• theorem witnessField_nonconstant L89
• def witnessGrad L106
• theorem hasDerivAt_sin_const_mul L109
• theorem witnessField_section_hasDerivAt L116
• def continuumTarget L132
• theorem continuumTarget_pos L136
• theorem witness_energy_density_eq L143
• theorem integral_cos_sq_two_pi L153
• theorem integral_witness_energy_density L187
• theorem witnessSample_addBit_true L210
• theorem stencil_inner_sum_witness L229
• theorem sum_cos_shifted_vanishes L244
• theorem sum_range_sq_sinDiff L300
• theorem freudenthalStencilEnergy_witness L354
• theorem scaledCanonicalEnergy_witness_closed_form L397
• def rateConstant L411
• theorem rateConstant_nonneg L413
• theorem witness_closed_form_dist L423
• theorem scaledCanonicalEnergy_witness_rate L449
• theorem freudenthal_witness_energy_limit L468
• theorem freudenthal_witness_energy_rate_integral_form L478
• theorem witness_closed_form_tendsto L491
• structure EnergyLimitStatus L511
• def energyLimitStatus L528