IndisputableMonolith.Applied.PhotobiomodulationDevice

declarations in this module (35)

• def planck_h L48
• def speed_of_light L51
• def eV_to_J L54
• lemma planck_h_pos L56
• lemma speed_of_light_pos L57
• lemma eV_to_J_pos L58
• def E_base L68
• lemma E_base_pos L70
• def phi_energy_rung L75
• lemma phi_energy_rung_pos L77
• theorem phi_energy_rung_step L81
• theorem phi_energy_rung_zero L88
• def E_PBM L99
• lemma E_PBM_pos L101
• lemma E_PBM_bounds L105
• theorem E_PBM_is_rung_6 L112
• lemma div_bounds_of_E_PBM L125
• def lambda_PBM L142
• lemma lambda_PBM_pos L144
• theorem lambda_PBM_in_therapeutic_window L149
• theorem lambda_PBM_approx L165
• def rs_pattern L200
• theorem rs_pattern_window_neutral L216
• structure WindowNeutralPattern L231
• def rs_neutral_pattern L236
• theorem rs_pattern_peak L240
• theorem rs_pattern_phi_components_neutral L243
• theorem rs_pattern_sqrt_components_neutral L250
• theorem phi_cubed_in_theta_band L268
• theorem phi_fifth_in_alpha_band L276
• theorem phi_eighth_in_gamma_band L283
• theorem modes_span_distinct_bands L288
• structure PBMDeviceSpec L301
• def rs_device L325
• theorem device_matches_octave L344