import PhysicsLogic.Framework.ThinViscousBoundaryLayerReduction

open PhysicsLogic.Framework.BoundaryLayerFieldReduction

example (field : ScalarField) (time x y : Real) :
    dt field time x y = deriv (fun t => field t x y) time := rfl
example (field : ScalarField) (time x y : Real) :
    dx field time x y = deriv (fun z => field time z y) x := rfl
example (field : ScalarField) (time x y : Real) :
    dy field time x y = deriv (fun z => field time x z) y := rfl
example (field : ScalarField) : dxx field = dx (dx field) := rfl
example (field : ScalarField) : dyy field = dy (dy field) := rfl

example (field : ScalarField) (time x y : Real) : FieldRegularAt field time x y =
    (DifferentiableAt Real (fun t => field t x y) time ∧
      DifferentiableAt Real (fun z => field time z y) x ∧
      DifferentiableAt Real (fun z => field time x z) y ∧
      DifferentiableAt Real (fun z => dx field time z y) x ∧
      DifferentiableAt Real (fun z => dy field time x z) y) := rfl

example (data : Data) (time x y : Real) : data.RegularAt time x y =
    (FieldRegularAt data.tangential time x y ∧ FieldRegularAt data.normal time x y ∧
      DifferentiableAt Real (fun z => data.pressure time z y) x ∧
      DifferentiableAt Real (fun z => data.pressure time x z) y ∧
      DifferentiableAt Real (data.outerPressure time) x) := rfl

example (data : Data) (time x y : Real) : data.tangentialAcceleration time x y =
    dt data.tangential time x y + data.tangential time x y * dx data.tangential time x y +
      data.normal time x y * dy data.tangential time x y := rfl

example (data : Data) (time x y : Real) : data.normalAcceleration time x y =
    dt data.normal time x y + data.tangential time x y * dx data.normal time x y +
      data.normal time x y * dy data.normal time x y := rfl

example (data : Data) (time x y : Real) : data.fullTangentialResidual time x y =
    data.density * data.tangentialAcceleration time x y + dx data.pressure time x y -
      data.viscosity * (dxx data.tangential time x y + dyy data.tangential time x y) := rfl

example (data : Data) (time x y : Real) : data.normalMechanicalResidual time x y =
    data.density * data.normalAcceleration time x y -
      data.viscosity * (dxx data.normal time x y + dyy data.normal time x y) := rfl

example (data : Data) (time x y : Real) : data.fullNormalResidual time x y =
    data.normalMechanicalResidual time x y + dy data.pressure time x y := rfl

example (data : Data) (time x y : Real) : data.continuityResidual time x y =
    dx data.tangential time x y + dy data.normal time x y := rfl

example (data : Data) (time x y : Real) : data.retainedTangentialResidual time x y =
    data.density * data.tangentialAcceleration time x y + deriv (data.outerPressure time) x -
      data.viscosity * dyy data.tangential time x y := rfl

example (data : Data) (time x y : Real) : data.steadyTangentialResidual time x y =
    data.density * (data.tangential time x y * dx data.tangential time x y +
      data.normal time x y * dy data.tangential time x y) + deriv (data.outerPressure time) x -
      data.viscosity * dyy data.tangential time x y := rfl

example (data : Data) (time x y : Real) : data.FullPlanarFlowAt time x y =
    (0 < data.density ∧ 0 < data.viscosity ∧ data.RegularAt time x y ∧
      data.fullTangentialResidual time x y = 0 ∧ data.fullNormalResidual time x y = 0 ∧
      data.continuityResidual time x y = 0) := rfl

example (data : Data) (time x y error : Real) : data.NonvacuousControlledReductionAt time x y error =
    (data.FullPlanarFlowAt time x y ∧ data.viscosity * dyy data.tangential time x y ≠ 0 ∧
      0 ≤ error ∧ |data.retainedTangentialResidual time x y| ≤ error) := rfl