import PhysicsLogic.Papers.PenziasWilson1965

/- Independent primitive specifications; no production proof is needed. -/
set_option autoImplicit false

open PhysicsLogic.Papers.PenziasWilson1965

example (readout : ProofStageSpectrumFormulaReadout) : readout.FormulaDomainAt ↔
    readout.lowFrequencyMegacyclesPerSecondValue < readout.highFrequencyMegacyclesPerSecondValue ∧
    0 < readout.highFrequencyResidualKelvinValue ∧
    0 < readout.lowFrequencyMegacyclesPerSecondValue ∧
    0 < readout.lowFrequencyMinimumKelvinValue ∧
    0 <= readout.maximumWavelengthPowerValue := Iff.rfl

example (readout : ProofStageSpectrumFormulaReadout) : readout.NoSteeperThanWavelengthPowerAt ↔
    readout.lowFrequencyMinimumKelvinValue / readout.highFrequencyResidualKelvinValue <=
      Real.rpow (readout.highFrequencyMegacyclesPerSecondValue /
        readout.lowFrequencyMegacyclesPerSecondValue) readout.maximumWavelengthPowerValue := Iff.rfl

example (spectrum : RadioSourceSpectrum) (readout : ProofStageSpectrumFormulaReadout) :
    spectrum.AccountsForWholeResidual readout ↔
      spectrum.highFrequencyKelvin = readout.highFrequencyResidualKelvinValue ∧
      0 <= spectrum.lowFrequencyKelvin ∧
      spectrum.lowFrequencyKelvin <= readout.lowFrequencyMinimumKelvinValue := Iff.rfl

example (spectrum : RadioSourceSpectrum) (readout : ProofStageSpectrumFormulaReadout) :
    spectrum.SteeperThanReadoutBound readout ↔
      0 < spectrum.highFrequencyKelvin ∧
      Real.rpow (readout.highFrequencyMegacyclesPerSecondValue /
        readout.lowFrequencyMegacyclesPerSecondValue) readout.maximumWavelengthPowerValue <
          spectrum.lowFrequencyKelvin / spectrum.highFrequencyKelvin := Iff.rfl