import PhysicsLogic.Papers.Hubble1929

set_option autoImplicit false
noncomputable section
open PhysicsLogic.Papers.Hubble1929
open scoped BigOperators
universe u
variable {Object : Type u}

example (x y z : Real) :
    (SolarReflexReadout.mk x y z).x = x ∧
      (SolarReflexReadout.mk x y z).y = y ∧ (SolarReflexReadout.mk x y z).z = z := ⟨rfl, rfl, rfl⟩

example (solar : SolarReflexReadout) (a d : Real) :
    solar.atDirection a d = solar.x * Real.cos a * Real.cos d +
      solar.y * Real.sin a * Real.cos d + solar.z * Real.sin d := rfl

example (v s k : Real) :
    (RadialVelocityReadout.mk v s k).observed = v ∧
      (RadialVelocityReadout.mk v s k).solarReflex = s ∧
      (RadialVelocityReadout.mk v s k).distanceEffect = k := ⟨rfl, rfl, rfl⟩

example (data : RadialVelocityReadout) : data.corrected = data.observed - data.solarReflex := rfl
example (data : RadialVelocityReadout) : data.peculiar = data.corrected - data.distanceEffect := rfl
example (data : RadialVelocityReadout) (residual : Real) :
    data.EquationOfConditionAt residual ↔ data.distanceEffect + data.solarReflex + residual = data.observed := Iff.rfl

open DistanceScaleCalibration

example (d v a z : Object -> Real) (s : SolarReflexReadout) (k : Real) :
    (Data.mk d v a z s k).distance = d ∧ (Data.mk d v a z s k).observedVelocity = v ∧
      (Data.mk d v a z s k).rightAscension = a ∧ (Data.mk d v a z s k).declination = z ∧
      (Data.mk d v a z s k).solar = s ∧ (Data.mk d v a z s k).coefficient = k :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩

example (data : Data Object) (object : Object) :
    data.radialReadout object = RadialVelocityReadout.mk (data.observedVelocity object)
      (data.solar.atDirection (data.rightAscension object) (data.declination object))
      (data.coefficient * data.distance object) := rfl

example (data : Data Object) (scale : Real) :
    data.rescaleDistance scale = Data.mk (fun object => scale * data.distance object)
      data.observedVelocity data.rightAscension data.declination data.solar (data.coefficient / scale) := rfl

example (data : Data Object) (sample : Set Object) (tolerance : Real) :
    data.PhysicalFitOn sample tolerance ↔
      sample.Finite ∧ sample.Nonempty ∧ 0 < data.coefficient ∧ 0 < tolerance ∧
        ∀ object ∈ sample, 0 < data.distance object ∧ |(data.radialReadout object).peculiar| ≤ tolerance := Iff.rfl

example (data : Data Object) (sample : Finset Object) (weight : Object -> Real) :
    data.weightedResidualLoss sample weight =
      ∑ object ∈ sample, weight object * (data.radialReadout object).peculiar ^ 2 := rfl

example (data : Data Object) :
    data.sharedRadialData = PhysicsLogic.Framework.NebularRadialData.mk
      data.distance data.observedVelocity
      (fun object => data.solar.atDirection (data.rightAscension object) (data.declination object))
      data.coefficient := rfl

example : Countermodels.control = Data.mk (fun object => if object = 0 then 1 else 2)
    (fun object => if object = 0 then 700 else 1050) (fun _ => 0) (fun _ => 0)
    (SolarReflexReadout.mk 100 0 0) 500 := rfl

example : PhysicsLogic.Papers.Hubble1929.NebularRelationFramework.Countermodels.ngc278TableTwoReadout =
    RadialVelocityReadout.mk 650 (-110) 760 := rfl