OAI/Analysis/Conductivity/Branching/CascadeGeometry.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.cascadePhase line 11
  2. lemma OAI.ScalarConductivity.cascadePhase_zero line 14
  3. lemma OAI.ScalarConductivity.cascadePhase_succ line 17
  4. lemma OAI.ScalarConductivity.cascadePhase_add line 23
  5. lemma OAI.ScalarConductivity.cascadePhase_antitone line 29
  6. lemma OAI.ScalarConductivity.cascadePhase_before line 40
  7. lemma OAI.ScalarConductivity.cascadePhase_after line 53
  8. lemma OAI.ScalarConductivity.cascadeProfile_only_two line 67
  9. lemma OAI.ScalarConductivity.cascadeProfile_terminal line 83
  10. lemma OAI.ScalarConductivity.exists_cascade_stage line 92
  11. def OAI.ScalarConductivity.cascadeAxis line 113
  12. lemma OAI.ScalarConductivity.cascadeAxis_ne_zero line 115
  13. lemma OAI.ScalarConductivity.cascadeAxis_succ line 119
  14. def OAI.ScalarConductivity.cascadeCenter line 123
  15. lemma OAI.ScalarConductivity.cascade_dilation_time line 126
  16. lemma OAI.ScalarConductivity.cascade_dilation_angular line 132
  17. def OAI.ScalarConductivity.cascadeTerm line 136
  18. def OAI.ScalarConductivity.cascadeValue line 140
  19. lemma OAI.ScalarConductivity.cascadeTerm_scaled line 142
  20. theorem OAI.ScalarConductivity.cascadeValue_C2 line 149
  21. lemma OAI.ScalarConductivity.cascadeValue_terminal line 163
  22. lemma OAI.ScalarConductivity.cascadeValue_two_modes line 171
  23. lemma OAI.ScalarConductivity.cascadeValue_zero_phase line 182